let n be Nat; :: thesis: for cB being Subset-Family of (TOP-REAL n) st cB = union (OpenHypercubesRAT n) holds
cB is quasi_basis
let F be Subset-Family of (TOP-REAL n); :: thesis: ( F = union (OpenHypercubesRAT n) implies F is quasi_basis )
assume A1: F = union (OpenHypercubesRAT n) ; :: thesis: F is quasi_basis
F is quasi_basis
proof
now :: thesis: for x being object st x in the topology of (TOP-REAL n) holds
x in UniCl F
let x be object ; :: thesis: ( x in the topology of (TOP-REAL n) implies x in UniCl F )
assume A2: x in the topology of (TOP-REAL n) ; :: thesis: x in UniCl F
then reconsider x1 = x as Subset of (TOP-REAL n) ;
A3: x1 is open by A2;
TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def 8;
then reconsider x2 = x1 as Subset of (TopSpaceMetr (Euclid n)) ;
A4: x2 is open by A3, Th10;
set Y = { t where t is Subset of (TOP-REAL n) : ( t in F & t c= x1 ) } ;
A5: { t where t is Subset of (TOP-REAL n) : ( t in F & t c= x1 ) } is Subset-Family of (TOP-REAL n)
proof
{ t where t is Subset of (TOP-REAL n) : ( t in F & t c= x1 ) } c= bool the carrier of (TOP-REAL n)
proof
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in { t where t is Subset of (TOP-REAL n) : ( t in F & t c= x1 ) } or t in bool the carrier of (TOP-REAL n) )
assume t in { t where t is Subset of (TOP-REAL n) : ( t in F & t c= x1 ) } ; :: thesis: t in bool the carrier of (TOP-REAL n)
then consider t0 being Subset of (TOP-REAL n) such that
A6: t = t0 and
t0 in F and
t0 c= x1 ;
thus t in bool the carrier of (TOP-REAL n) by A6; :: thesis: verum
end;
hence { t where t is Subset of (TOP-REAL n) : ( t in F & t c= x1 ) } is Subset-Family of (TOP-REAL n) ; :: thesis: verum
end;
A7: { t where t is Subset of (TOP-REAL n) : ( t in F & t c= x1 ) } c= F
proof
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in { t where t is Subset of (TOP-REAL n) : ( t in F & t c= x1 ) } or t in F )
assume t in { t where t is Subset of (TOP-REAL n) : ( t in F & t c= x1 ) } ; :: thesis: t in F
then consider t0 being Subset of (TOP-REAL n) such that
A8: t = t0 and
A9: t0 in F and
t0 c= x1 ;
thus t in F by A8, A9; :: thesis: verum
end;
x = union { t where t is Subset of (TOP-REAL n) : ( t in F & t c= x1 ) }
proof
reconsider x3 = x as set by TARSKI:1;
A10: x3 c= union { t where t is Subset of (TOP-REAL n) : ( t in F & t c= x1 ) }
proof
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in x3 or t in union { t where t is Subset of (TOP-REAL n) : ( t in F & t c= x1 ) } )
assume A11: t in x3 ; :: thesis: t in union { t where t is Subset of (TOP-REAL n) : ( t in F & t c= x1 ) }
then t in x2 ;
then reconsider t1 = t as Point of (Euclid n) ;
consider m1 being non zero Element of NAT such that
A12: OpenHypercube (t1,(1 / m1)) c= x2 by A4, A11, EUCLID_9:23;
reconsider t2 = t1 as Point of (TOP-REAL n) by EUCLID:67;
reconsider Invm1Div2 = (1 / m1) / 2 as positive Real ;
consider e being Point of (Euclid n) such that
t2 = e and
A13: OpenHypercube (t2,((1 / m1) / 2)) = OpenHypercube (e,((1 / m1) / 2)) by TIETZE_2:def 1;
consider q0 being Element of RAT n such that
A14: q0 in OpenHypercube (t2,Invm1Div2) by A13, Th20;
( q0 in RAT n & RAT n is Subset of (REAL n) ) by NUMBERS:12, Th5;
then reconsider q1 = q0 as Point of (TOP-REAL n) by EUCLID:22;
reconsider r = Invm1Div2 * 2 as Real ;
A15: OpenHypercube (q1,(r / 2)) c= OpenHypercube (t2,r) by A14, Th12;
reconsider q2 = q1 as Point of (Euclid n) by EUCLID:67;
set OO = OpenHypercube (q2,Invm1Div2);
A16: now :: thesis: ( OpenHypercube (t2,r) = OpenHypercube (t2,(1 / m1)) & OpenHypercube (t1,(1 / m1)) = OpenHypercube (t2,(1 / m1)) & OpenHypercube (t1,(1 / m1)) c= x1 )
thus OpenHypercube (t2,r) = OpenHypercube (t2,(1 / m1)) ; :: thesis: ( OpenHypercube (t1,(1 / m1)) = OpenHypercube (t2,(1 / m1)) & OpenHypercube (t1,(1 / m1)) c= x1 )
consider ez being Point of (Euclid n) such that
A17: t2 = ez and
A18: OpenHypercube (t2,(1 / m1)) = OpenHypercube (ez,(1 / m1)) by TIETZE_2:def 1;
thus OpenHypercube (t1,(1 / m1)) = OpenHypercube (t2,(1 / m1)) by A17, A18; :: thesis: OpenHypercube (t1,(1 / m1)) c= x1
thus OpenHypercube (t1,(1 / m1)) c= x1 by A12; :: thesis: verum
end;
consider er being Point of (Euclid n) such that
A19: q2 = er and
A20: OpenHypercube (q1,Invm1Div2) = OpenHypercube (er,Invm1Div2) by TIETZE_2:def 1;
A21: Invm1Div2 = 1 / (m1 * 2) by XCMPLX_1:78;
A22: OpenHypercube (q2,Invm1Div2) in union (OpenHypercubesRAT n)
proof
consider e being Point of (Euclid n) such that
A23: q2 = e and
OpenHypercube (q2,Invm1Div2) = OpenHypercube (e,Invm1Div2) ;
A24: OpenHypercube (q2,Invm1Div2) in OpenHypercubes e by A21, A23;
OpenHypercubes e in OpenHypercubesRAT n by A23;
hence OpenHypercube (q2,Invm1Div2) in union (OpenHypercubesRAT n) by A24, TARSKI:def 4; :: thesis: verum
end;
( t in OpenHypercube (q2,Invm1Div2) & OpenHypercube (q2,Invm1Div2) in F & OpenHypercube (q2,Invm1Div2) c= x1 ) by A22, A1, A19, A20, A14, Th11, A15, A16;
then ( t in OpenHypercube (q2,Invm1Div2) & OpenHypercube (q2,Invm1Div2) in { t where t is Subset of (TOP-REAL n) : ( t in F & t c= x1 ) } ) ;
hence t in union { t where t is Subset of (TOP-REAL n) : ( t in F & t c= x1 ) } by TARSKI:def 4; :: thesis: verum
end;
union { t where t is Subset of (TOP-REAL n) : ( t in F & t c= x1 ) } c= x1
proof
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in union { t where t is Subset of (TOP-REAL n) : ( t in F & t c= x1 ) } or t in x1 )
assume t in union { t where t is Subset of (TOP-REAL n) : ( t in F & t c= x1 ) } ; :: thesis: t in x1
then consider Z being set such that
A25: t in Z and
A26: Z in { t where t is Subset of (TOP-REAL n) : ( t in F & t c= x1 ) } by TARSKI:def 4;
consider t0 being Subset of (TOP-REAL n) such that
A27: Z = t0 and
t0 in F and
A28: t0 c= x1 by A26;
thus t in x1 by A25, A27, A28; :: thesis: verum
end;
then x1 = union { t where t is Subset of (TOP-REAL n) : ( t in F & t c= x1 ) } by A10;
hence x = union { t where t is Subset of (TOP-REAL n) : ( t in F & t c= x1 ) } ; :: thesis: verum
end;
hence x in UniCl F by A5, A7, CANTOR_1:def 1; :: thesis: verum
end;
then the topology of (TOP-REAL n) c= UniCl F ;
hence F is quasi_basis by CANTOR_1:def 2; :: thesis: verum
end;
hence F is quasi_basis ; :: thesis: verum