let T be non empty normal TopSpace; :: thesis: for A, B being closed Subset of T st A <> {} & A misses B holds
for G being Rain of A,B
for r being Real
for C being Subset of T st C = (Tempest G) . r & r in DOM holds
C is open
let A, B be closed Subset of T; :: thesis: ( A <> {} & A misses B implies for G being Rain of A,B
for r being Real
for C being Subset of T st C = (Tempest G) . r & r in DOM holds
C is open )
assume A1: ( A <> {} & A misses B ) ; :: thesis: for G being Rain of A,B
for r being Real
for C being Subset of T st C = (Tempest G) . r & r in DOM holds
C is open
let G be Rain of A,B; :: thesis: for r being Real
for C being Subset of T st C = (Tempest G) . r & r in DOM holds
C is open
let r be Real; :: thesis: for C being Subset of T st C = (Tempest G) . r & r in DOM holds
C is open
let C be Subset of T; :: thesis: ( C = (Tempest G) . r & r in DOM implies C is open )
assume that
A2: C = (Tempest G) . r and
A3: r in DOM ; :: thesis: C is open
A4: ( r in (halfline 0) \/ DYADIC or r in right_open_halfline 1 ) by A3, URYSOHN1:def 3, XBOOLE_0:def 3;
per cases ( r in halfline 0 or r in DYADIC or r in right_open_halfline 1 ) by A4, XBOOLE_0:def 3;
suppose r in halfline 0 ; :: thesis: C is open
then C = {} by A1, A2, A3, Def4;
then C in the topology of T by PRE_TOPC:1;
hence C is open ; :: thesis: verum
end;
suppose A5: r in DYADIC ; :: thesis: C is open
then consider n being Nat such that
A6: r in dyadic n by URYSOHN1:def 2;
reconsider D = G . n as Drizzle of A,B,n by A1, Def2;
A7: for r1, r2 being Element of dyadic n st r1 < r2 holds
( D . r1 is open & D . r2 is open & Cl (D . r1) c= D . r2 & A c= D . 0 & B = ([#] T) \ (D . 1) ) by A1, Def1;
A8: (Tempest G) . r = (G . n) . r by A1, A3, A5, A6, Def4;
now :: thesis: ( ( r = 0 & C is open ) or ( 0 < r & C is open ) )
per cases ( r = 0 or 0 < r ) by A6, URYSOHN1:1;
case A9: r = 0 ; :: thesis: C is open
then reconsider r = r as Element of dyadic n by URYSOHN1:6;
( 1 is Element of dyadic n & D . r = C ) by A1, A2, A3, A5, Def4, URYSOHN1:6;
hence C is open by A1, A9, Def1; :: thesis: verum
end;
end;
end;
hence C is open ; :: thesis: verum
end;
suppose A11: r in right_open_halfline 1 ; :: thesis: C is open
A12: the carrier of T in the topology of T by PRE_TOPC:def 1;
C = the carrier of T by A1, A2, A3, A11, Def4;
hence C is open by A12; :: thesis: verum
end;
end;