A1:
1 in dyadic 0
by TARSKI:def 2, URYSOHN1:2;
then A2:
1 in DYADIC
by URYSOHN1:def 2;
then
1 in (halfline 0) \/ DYADIC
by XBOOLE_0:def 3;
then A3:
1 in DOM
by URYSOHN1:def 3, XBOOLE_0:def 3;
reconsider e1 = 1 as R_eal by XXREAL_0:def 1;
let T be non empty normal TopSpace; for A, B being closed Subset of T st A <> {} & A misses B holds
for G being Rain of A,B holds
( Thunder G is continuous & ( for x being Point of T holds
( 0 <= (Thunder G) . x & (Thunder G) . x <= 1 & ( x in A implies (Thunder G) . x = 0 ) & ( x in B implies (Thunder G) . x = 1 ) ) ) )
let A, B be closed Subset of T; ( A <> {} & A misses B implies for G being Rain of A,B holds
( Thunder G is continuous & ( for x being Point of T holds
( 0 <= (Thunder G) . x & (Thunder G) . x <= 1 & ( x in A implies (Thunder G) . x = 0 ) & ( x in B implies (Thunder G) . x = 1 ) ) ) ) )
assume A4:
( A <> {} & A misses B )
; for G being Rain of A,B holds
( Thunder G is continuous & ( for x being Point of T holds
( 0 <= (Thunder G) . x & (Thunder G) . x <= 1 & ( x in A implies (Thunder G) . x = 0 ) & ( x in B implies (Thunder G) . x = 1 ) ) ) )
let G be Rain of A,B; ( Thunder G is continuous & ( for x being Point of T holds
( 0 <= (Thunder G) . x & (Thunder G) . x <= 1 & ( x in A implies (Thunder G) . x = 0 ) & ( x in B implies (Thunder G) . x = 1 ) ) ) )
A5:
0 in dyadic 0
by TARSKI:def 2, URYSOHN1:2;
then A6:
0 in DYADIC
by URYSOHN1:def 2;
then
0 in (halfline 0) \/ DYADIC
by XBOOLE_0:def 3;
then A7:
0 in DOM
by URYSOHN1:def 3, XBOOLE_0:def 3;
A8:
for x being Point of T holds
( 0 <= (Thunder G) . x & (Thunder G) . x <= 1 & ( x in A implies (Thunder G) . x = 0 ) & ( x in B implies (Thunder G) . x = 1 ) )
proof
let x be
Point of
T;
( 0 <= (Thunder G) . x & (Thunder G) . x <= 1 & ( x in A implies (Thunder G) . x = 0 ) & ( x in B implies (Thunder G) . x = 1 ) )
now ( ( Rainbow (x,G) = {} & 0 <= (Thunder G) . x & (Thunder G) . x <= 1 & ( x in A implies (Thunder G) . x = 0 ) & ( x in B implies (Thunder G) . x = 1 ) ) or ( Rainbow (x,G) <> {} & 0 <= (Thunder G) . x & (Thunder G) . x <= 1 & ( x in A implies (Thunder G) . x = 0 ) & ( x in B implies (Thunder G) . x = 1 ) ) )per cases
( Rainbow (x,G) = {} or Rainbow (x,G) <> {} )
;
case A9:
Rainbow (
x,
G)
= {}
;
( 0 <= (Thunder G) . x & (Thunder G) . x <= 1 & ( x in A implies (Thunder G) . x = 0 ) & ( x in B implies (Thunder G) . x = 1 ) )
(
x in B implies
(Thunder G) . x = 1 )
proof
G . 0 is
Drizzle of
A,
B,
0
by A4, Def2;
then A10:
B = ([#] T) \ ((G . 0) . 1)
by A4, Def1;
assume A11:
x in B
;
(Thunder G) . x = 1
(Tempest G) . 1
= (G . 0) . 1
by A4, A1, A2, A3, Def4;
then
for
s being
Real st
s = 1 holds
not
x in (Tempest G) . s
by A11, A10, XBOOLE_0:def 5;
hence
(Thunder G) . x = 1
by A9, Def5, URYSOHN2:27;
verum
end; hence
(
0 <= (Thunder G) . x &
(Thunder G) . x <= 1 & (
x in A implies
(Thunder G) . x = 0 ) & (
x in B implies
(Thunder G) . x = 1 ) )
by A9, Def6;
verum end; case A12:
Rainbow (
x,
G)
<> {}
;
( 0 <= (Thunder G) . x & (Thunder G) . x <= 1 & ( x in A implies (Thunder G) . x = 0 ) & ( x in B implies (Thunder G) . x = 1 ) )A13:
(
x in A implies
(Thunder G) . x = 0 )
proof
assume A14:
x in A
;
(Thunder G) . x = 0
A15:
for
s being
R_eal st
0. < s holds
not
s in Rainbow (
x,
G)
proof
let s be
R_eal;
( 0. < s implies not s in Rainbow (x,G) )
assume
0. < s
;
not s in Rainbow (x,G)
assume A16:
s in Rainbow (
x,
G)
;
contradiction
then A17:
s in DYADIC
by Def5;
then reconsider s =
s as
Real ;
consider n being
Nat such that A18:
s in dyadic n
by A17, URYSOHN1:def 2;
s in (halfline 0) \/ DYADIC
by A17, XBOOLE_0:def 3;
then
s in DOM
by URYSOHN1:def 3, XBOOLE_0:def 3;
then A19:
(Tempest G) . s = (G . n) . s
by A4, A17, A18, Def4;
reconsider r1 =
0 ,
r2 =
s as
Element of
dyadic n by A18, URYSOHN1:6;
reconsider D =
G . n as
Drizzle of
A,
B,
n by A4, Def2;
end;
G . 0 is
Drizzle of
A,
B,
0
by A4, Def2;
then A24:
A c= (G . 0) . 0
by A4, Def1;
A25:
(Tempest G) . 0 = (G . 0) . 0
by A4, A5, A6, A7, Def4;
consider a being
object such that A26:
a in Rainbow (
x,
G)
by A12, XBOOLE_0:def 1;
A27:
a in DYADIC
by A26, Def5;
then reconsider a =
a as
Real ;
A28:
ex
n being
Nat st
a in dyadic n
by A27, URYSOHN1:def 2;
end; reconsider S =
Rainbow (
x,
G) as non
empty Subset of
ExtREAL by A12;
A29:
sup S <= e1
by Th14;
A30:
(
x in B implies
(Thunder G) . x = 1 )
proof
G . 0 is
Drizzle of
A,
B,
0
by A4, Def2;
then A31:
B = ([#] T) \ ((G . 0) . 1)
by A4, Def1;
assume A32:
x in B
;
(Thunder G) . x = 1
(Tempest G) . 1
= (G . 0) . 1
by A4, A1, A2, A3, Def4;
then A33:
for
s being
Real st
s = 1 holds
not
x in (Tempest G) . s
by A32, A31, XBOOLE_0:def 5;
then reconsider S =
Rainbow (
x,
G) as non
empty Subset of
ExtREAL by Def5, URYSOHN2:27;
1
in Rainbow (
x,
G)
by A33, Def5, URYSOHN2:27;
then A34:
e1 <= sup S
by XXREAL_2:4;
(Thunder G) . x = sup S
by Def6;
hence
(Thunder G) . x = 1
by A29, A34, XXREAL_0:1;
verum
end;
(
e1 = 1 &
(Thunder G) . x = sup S )
by Def6;
hence
(
0 <= (Thunder G) . x &
(Thunder G) . x <= 1 & (
x in A implies
(Thunder G) . x = 0 ) & (
x in B implies
(Thunder G) . x = 1 ) )
by A13, A30, Th14;
verum end; end; end;
hence
(
0 <= (Thunder G) . x &
(Thunder G) . x <= 1 & (
x in A implies
(Thunder G) . x = 0 ) & (
x in B implies
(Thunder G) . x = 1 ) )
;
verum
end;
for p being Point of T holds Thunder G is_continuous_at p
proof
let p be
Point of
T;
Thunder G is_continuous_at p
for
Q being
Subset of
R^1 st
Q is
open &
(Thunder G) . p in Q holds
ex
H being
Subset of
T st
(
H is
open &
p in H &
(Thunder G) .: H c= Q )
proof
let Q be
Subset of
R^1;
( Q is open & (Thunder G) . p in Q implies ex H being Subset of T st
( H is open & p in H & (Thunder G) .: H c= Q ) )
assume that A35:
Q is
open
and A36:
(Thunder G) . p in Q
;
ex H being Subset of T st
( H is open & p in H & (Thunder G) .: H c= Q )
reconsider x =
(Thunder G) . p as
Element of
RealSpace by A36, TOPMETR:12, TOPMETR:def 6;
reconsider Q =
Q as
Subset of
REAL by TOPMETR:17;
( the
topology of
R^1 = Family_open_set RealSpace &
Q in the
topology of
R^1 )
by A35, TOPMETR:12, TOPMETR:def 6;
then consider r being
Real such that A37:
r > 0
and A38:
Ball (
x,
r)
c= Q
by A36, PCOMPS_1:def 4;
ex
r0 being
Real st
(
r0 < r &
0 < r0 &
r0 <= 1 )
then consider r0 being
Real such that A41:
r0 < r
and A42:
(
0 < r0 &
r0 <= 1 )
;
consider r1 being
Real such that A43:
r1 in DYADIC
and A44:
0 < r1
and A45:
r1 < r0
by A42, URYSOHN2:24;
A46:
r1 in DYADIC \/ (right_open_halfline 1)
by A43, XBOOLE_0:def 3;
consider n being
Nat such that A47:
r1 in dyadic n
by A43, URYSOHN1:def 2;
reconsider D =
G . n as
Drizzle of
A,
B,
n by A4, Def2;
r1 in (halfline 0) \/ DYADIC
by A43, XBOOLE_0:def 3;
then A48:
r1 in DOM
by URYSOHN1:def 3, XBOOLE_0:def 3;
then A49:
(Tempest G) . r1 = (G . n) . r1
by A4, A43, A47, Def4;
A50:
r1 < r
by A41, A45, XXREAL_0:2;
A51:
for
p being
Point of
T st
p in (Tempest G) . r1 holds
(Thunder G) . p < r
A52:
the
carrier of
R^1 = the
carrier of
RealSpace
by TOPMETR:12, TOPMETR:def 6;
reconsider r1 =
r1 as
Element of
dyadic n by A47;
reconsider H =
D . r1 as
Subset of
T ;
A53:
0 in dyadic n
by URYSOHN1:6;
ex
H being
Subset of
T st
(
H is
open &
p in H &
(Thunder G) .: H c= Q )
proof
per cases
( x = 0 or x <> 0 )
;
suppose A54:
x = 0
;
ex H being Subset of T st
( H is open & p in H & (Thunder G) .: H c= Q )take
H
;
( H is open & p in H & (Thunder G) .: H c= Q )
(Thunder G) .: H c= Q
proof
reconsider p =
x as
Real ;
let y be
object ;
TARSKI:def 3 ( not y in (Thunder G) .: H or y in Q )
assume
y in (Thunder G) .: H
;
y in Q
then consider x1 being
object such that
x1 in dom (Thunder G)
and A55:
x1 in H
and A56:
y = (Thunder G) . x1
by FUNCT_1:def 6;
reconsider y =
y as
Point of
RealSpace by A52, A55, A56, FUNCT_2:5;
reconsider q =
y as
Real ;
A57:
- (p - q) < r
by A51, A49, A54, A55, A56;
reconsider x1 =
x1 as
Point of
T by A55;
A58:
0 <= (Thunder G) . x1
by A8;
A59:
q - p < r - 0
by A51, A49, A54, A55, A56;
then
p - q < r
by A54, A56, A58, XREAL_1:14;
then A60:
|.(p - q).| <> r
by A57, ABSVALUE:def 1;
A61:
(
dist (
x,
y)
< r implies
y in Ball (
x,
r) )
by METRIC_1:11;
- (- (p - q)) = p - q
;
then
- r < p - q
by A57, XREAL_1:24;
then
(
dist (
x,
y)
= |.(p - q).| &
|.(p - q).| <= r )
by A54, A56, A58, A59, ABSVALUE:5, TOPMETR:11;
hence
y in Q
by A38, A61, A60, XXREAL_0:1;
verum
end; hence
(
H is
open &
p in H &
(Thunder G) .: H c= Q )
by A4, A44, A48, A49, A53, A54, Def1, Th15;
verum end; suppose A62:
x <> 0
;
ex H being Subset of T st
( H is open & p in H & (Thunder G) .: H c= Q )reconsider x =
x as
Real ;
0 <= (Thunder G) . p
by A8;
then consider r1,
r2 being
Real such that A63:
r1 in DYADIC \/ (right_open_halfline 1)
and
r2 in DYADIC \/ (right_open_halfline 1)
and A64:
0 < r1
and A65:
r1 < x
and A66:
x < r2
and A67:
r2 - r1 < r
by A37, A62, URYSOHN2:31;
(
r1 in DYADIC or
r1 in right_open_halfline 1 )
by A63, XBOOLE_0:def 3;
then
(
r1 in (halfline 0) \/ DYADIC or
r1 in right_open_halfline 1 )
by XBOOLE_0:def 3;
then A68:
r1 in DOM
by URYSOHN1:def 3, XBOOLE_0:def 3;
then reconsider B =
(Tempest G) . r1 as
Subset of
T by FUNCT_2:5;
reconsider C =
([#] T) \ (Cl B) as
Subset of
T ;
consider r3 being
Real such that A69:
r3 in DOM
and A70:
x < r3
and A71:
r3 < r2
by A66, URYSOHN2:25;
Cl (Cl B) = Cl B
;
then
Cl B is
closed
by PRE_TOPC:22;
then A72:
C is
open
;
reconsider A =
(Tempest G) . r3 as
Subset of
T by A69, FUNCT_2:5;
take H =
A /\ C;
( H is open & p in H & (Thunder G) .: H c= Q )A73:
(Thunder G) .: H c= Q
proof
reconsider x =
x as
Element of
RealSpace ;
let y be
object ;
TARSKI:def 3 ( not y in (Thunder G) .: H or y in Q )
reconsider p =
x as
Real ;
assume
y in (Thunder G) .: H
;
y in Q
then consider x1 being
object such that
x1 in dom (Thunder G)
and A74:
x1 in H
and A75:
y = (Thunder G) . x1
by FUNCT_1:def 6;
reconsider x1 =
x1 as
Point of
T by A74;
A76:
x1 in (Tempest G) . r3
by A74, XBOOLE_0:def 4;
reconsider y =
y as
Real by A75;
reconsider y =
y as
Point of
RealSpace by A52, A74, A75, FUNCT_2:5;
reconsider q =
y as
Real ;
A77:
- (- (p - q)) = p - q
;
A78:
not
r3 <= 0
by A8, A70;
(
r3 in (halfline 0) \/ DYADIC or
r3 in right_open_halfline 1 )
by A69, URYSOHN1:def 3, XBOOLE_0:def 3;
then
(
r3 in halfline 0 or
r3 in DYADIC or
r3 in right_open_halfline 1 )
by XBOOLE_0:def 3;
then
r3 in DYADIC \/ (right_open_halfline 1)
by A78, XBOOLE_0:def 3, XXREAL_1:233;
then
(Thunder G) . x1 <= r3
by A4, A76, A78, Th16;
then
(Thunder G) . x1 < r2
by A71, XXREAL_0:2;
then A79:
q - p < r2 - r1
by A65, A75, XREAL_1:14;
then
- (p - q) < r
by A67, XXREAL_0:2;
then A80:
- r < p - q
by A77, XREAL_1:24;
A81:
x1 in ([#] T) \ (Cl B)
by A74, XBOOLE_0:def 4;
not
x1 in B
then A83:
p - q < r2 - r1
by A4, A66, A68, A75, Th15, XREAL_1:14;
then
p - q < r
by A67, XXREAL_0:2;
then A84:
(
dist (
x,
y)
= |.(p - q).| &
|.(p - q).| <= r )
by A80, ABSVALUE:5, TOPMETR:11;
A85:
|.(p - q).| <> r
(
dist (
x,
y)
< r implies
y in Ball (
x,
r) )
by METRIC_1:11;
hence
y in Q
by A38, A84, A85, XXREAL_0:1;
verum
end;
(Thunder G) . p <= 1
by A8;
then consider r4 being
Real such that A87:
r4 in DYADIC
and A88:
r1 < r4
and A89:
r4 < x
by A64, A65, URYSOHN2:24;
A90:
r4 in (halfline 0) \/ DYADIC
by A87, XBOOLE_0:def 3;
then
r4 in DOM
by URYSOHN1:def 3, XBOOLE_0:def 3;
then A91:
Cl B c= (Tempest G) . r4
by A4, A88, A68, Th12;
reconsider r4 =
r4 as
Element of
DOM by A90, URYSOHN1:def 3, XBOOLE_0:def 3;
not
p in (Tempest G) . r4
by A4, A64, A88, A89, Th17;
then
not
p in Cl B
by A91;
then A92:
p in C
by XBOOLE_0:def 5;
(
A is
open &
p in (Tempest G) . r3 )
by A4, A69, A70, Th11, Th15;
hence
(
H is
open &
p in H &
(Thunder G) .: H c= Q )
by A72, A92, A73, TOPS_1:11, XBOOLE_0:def 4;
verum end; end;
end;
hence
ex
H being
Subset of
T st
(
H is
open &
p in H &
(Thunder G) .: H c= Q )
;
verum
end;
hence
Thunder G is_continuous_at p
by TMAP_1:43;
verum
end;
hence
( Thunder G is continuous & ( for x being Point of T holds
( 0 <= (Thunder G) . x & (Thunder G) . x <= 1 & ( x in A implies (Thunder G) . x = 0 ) & ( x in B implies (Thunder G) . x = 1 ) ) ) )
by A8, TMAP_1:44; verum