:: CANTOR_1 semantic presentation
begin
definition
let X be set ;
let A be Subset-Family of X;
func UniCl A -> Subset-Family of X means :Def1: :: CANTOR_1:def 1
for x being Subset of X holds
( x in it iff ex Y being Subset-Family of X st
( Y c= A & x = union Y ) );
existence
ex b1 being Subset-Family of X st
for x being Subset of X holds
( x in b1 iff ex Y being Subset-Family of X st
( Y c= A & x = union Y ) )
proof
defpred S1[ set ] means ex Y being Subset-Family of X st
( Y c= A & $1 = union Y );
ex Z being Subset-Family of X st
for x being Subset of X holds
( x in Z iff S1[x] ) from SUBSET_1:sch_3();
hence ex b1 being Subset-Family of X st
for x being Subset of X holds
( x in b1 iff ex Y being Subset-Family of X st
( Y c= A & x = union Y ) ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being Subset-Family of X st ( for x being Subset of X holds
( x in b1 iff ex Y being Subset-Family of X st
( Y c= A & x = union Y ) ) ) & ( for x being Subset of X holds
( x in b2 iff ex Y being Subset-Family of X st
( Y c= A & x = union Y ) ) ) holds
b1 = b2
proof
let F1, F2 be Subset-Family of X; ::_thesis: ( ( for x being Subset of X holds
( x in F1 iff ex Y being Subset-Family of X st
( Y c= A & x = union Y ) ) ) & ( for x being Subset of X holds
( x in F2 iff ex Y being Subset-Family of X st
( Y c= A & x = union Y ) ) ) implies F1 = F2 )
assume that
A1: for x being Subset of X holds
( x in F1 iff ex Y being Subset-Family of X st
( Y c= A & x = union Y ) ) and
A2: for x being Subset of X holds
( x in F2 iff ex Y being Subset-Family of X st
( Y c= A & x = union Y ) ) ; ::_thesis: F1 = F2
now__::_thesis:_for_x_being_Subset_of_X_holds_
(_x_in_F1_iff_x_in_F2_)
let x be Subset of X; ::_thesis: ( x in F1 iff x in F2 )
( x in F1 iff ex Y being Subset-Family of X st
( Y c= A & x = union Y ) ) by A1;
hence ( x in F1 iff x in F2 ) by A2; ::_thesis: verum
end;
hence F1 = F2 by SUBSET_1:3; ::_thesis: verum
end;
end;
:: deftheorem Def1 defines UniCl CANTOR_1:def_1_:_
for X being set
for A, b3 being Subset-Family of X holds
( b3 = UniCl A iff for x being Subset of X holds
( x in b3 iff ex Y being Subset-Family of X st
( Y c= A & x = union Y ) ) );
definition
let X be TopStruct ;
let F be Subset-Family of X;
attrF is quasi_basis means :Def2: :: CANTOR_1:def 2
the topology of X c= UniCl F;
end;
:: deftheorem Def2 defines quasi_basis CANTOR_1:def_2_:_
for X being TopStruct
for F being Subset-Family of X holds
( F is quasi_basis iff the topology of X c= UniCl F );
registration
let X be TopStruct ;
cluster the topology of X -> quasi_basis ;
coherence
the topology of X is quasi_basis
proof
set F = the topology of X;
let A be set ; :: according to TARSKI:def_3,CANTOR_1:def_2 ::_thesis: ( not A in the topology of X or A in UniCl the topology of X )
assume A1: A in the topology of X ; ::_thesis: A in UniCl the topology of X
then reconsider B = {A} as Subset-Family of X by SUBSET_1:41;
A2: B c= the topology of X by A1, ZFMISC_1:31;
A = union B by ZFMISC_1:25;
hence A in UniCl the topology of X by A2, Def1; ::_thesis: verum
end;
end;
registration
let X be TopStruct ;
cluster open quasi_basis for Element of bool (bool the carrier of X);
existence
ex b1 being Subset-Family of X st
( b1 is open & b1 is quasi_basis )
proof
take the topology of X ; ::_thesis: ( the topology of X is open & the topology of X is quasi_basis )
thus ( the topology of X is open & the topology of X is quasi_basis ) ; ::_thesis: verum
end;
end;
definition
let X be TopStruct ;
mode Basis of X is open quasi_basis Subset-Family of X;
end;
theorem Th1: :: CANTOR_1:1
for X being set
for A being Subset-Family of X holds A c= UniCl A
proof
let X be set ; ::_thesis: for A being Subset-Family of X holds A c= UniCl A
let A be Subset-Family of X; ::_thesis: A c= UniCl A
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in UniCl A )
assume A1: x in A ; ::_thesis: x in UniCl A
then reconsider x9 = x as Subset of X ;
reconsider s = {x9} as Subset-Family of X by SUBSET_1:41;
A2: x = union s by ZFMISC_1:25;
s c= A by A1, ZFMISC_1:31;
hence x in UniCl A by A2, Def1; ::_thesis: verum
end;
theorem :: CANTOR_1:2
for S being TopStruct holds the topology of S is Basis of S ;
theorem :: CANTOR_1:3
for S being TopStruct holds the topology of S is open ;
definition
let X be set ;
let A be Subset-Family of X;
func FinMeetCl A -> Subset-Family of X means :Def3: :: CANTOR_1:def 3
for x being Subset of X holds
( x in it iff ex Y being Subset-Family of X st
( Y c= A & Y is finite & x = Intersect Y ) );
existence
ex b1 being Subset-Family of X st
for x being Subset of X holds
( x in b1 iff ex Y being Subset-Family of X st
( Y c= A & Y is finite & x = Intersect Y ) )
proof
defpred S1[ set ] means ex Y being Subset-Family of X st
( Y c= A & Y is finite & $1 = Intersect Y );
ex Z being Subset-Family of X st
for x being Subset of X holds
( x in Z iff S1[x] ) from SUBSET_1:sch_3();
hence ex b1 being Subset-Family of X st
for x being Subset of X holds
( x in b1 iff ex Y being Subset-Family of X st
( Y c= A & Y is finite & x = Intersect Y ) ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being Subset-Family of X st ( for x being Subset of X holds
( x in b1 iff ex Y being Subset-Family of X st
( Y c= A & Y is finite & x = Intersect Y ) ) ) & ( for x being Subset of X holds
( x in b2 iff ex Y being Subset-Family of X st
( Y c= A & Y is finite & x = Intersect Y ) ) ) holds
b1 = b2
proof
let B1, B2 be Subset-Family of X; ::_thesis: ( ( for x being Subset of X holds
( x in B1 iff ex Y being Subset-Family of X st
( Y c= A & Y is finite & x = Intersect Y ) ) ) & ( for x being Subset of X holds
( x in B2 iff ex Y being Subset-Family of X st
( Y c= A & Y is finite & x = Intersect Y ) ) ) implies B1 = B2 )
assume that
A1: for x being Subset of X holds
( x in B1 iff ex Y being Subset-Family of X st
( Y c= A & Y is finite & x = Intersect Y ) ) and
A2: for x being Subset of X holds
( x in B2 iff ex Y being Subset-Family of X st
( Y c= A & Y is finite & x = Intersect Y ) ) ; ::_thesis: B1 = B2
now__::_thesis:_for_x_being_Subset_of_X_holds_
(_x_in_B2_iff_x_in_B1_)
let x be Subset of X; ::_thesis: ( x in B2 iff x in B1 )
( x in B2 iff ex Y being Subset-Family of X st
( Y c= A & Y is finite & x = Intersect Y ) ) by A2;
hence ( x in B2 iff x in B1 ) by A1; ::_thesis: verum
end;
hence B1 = B2 by SUBSET_1:3; ::_thesis: verum
end;
end;
:: deftheorem Def3 defines FinMeetCl CANTOR_1:def_3_:_
for X being set
for A, b3 being Subset-Family of X holds
( b3 = FinMeetCl A iff for x being Subset of X holds
( x in b3 iff ex Y being Subset-Family of X st
( Y c= A & Y is finite & x = Intersect Y ) ) );
theorem Th4: :: CANTOR_1:4
for X being set
for A being Subset-Family of X holds A c= FinMeetCl A
proof
let X be set ; ::_thesis: for A being Subset-Family of X holds A c= FinMeetCl A
let A be Subset-Family of X; ::_thesis: A c= FinMeetCl A
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in FinMeetCl A )
assume A1: x in A ; ::_thesis: x in FinMeetCl A
then reconsider x9 = x as Subset of X ;
reconsider s = {x9} as Subset-Family of X by SUBSET_1:41;
x = meet s by SETFAM_1:10;
then A2: x = Intersect s by SETFAM_1:def_9;
s c= A by A1, ZFMISC_1:31;
hence x in FinMeetCl A by A2, Def3; ::_thesis: verum
end;
theorem Th5: :: CANTOR_1:5
for T being non empty TopSpace holds the topology of T = FinMeetCl the topology of T
proof
let T be non empty TopSpace; ::_thesis: the topology of T = FinMeetCl the topology of T
set X = the topology of T;
defpred S1[ set ] means meet $1 in the topology of T;
A1: for B9 being Element of Fin the topology of T
for b being Element of the topology of T st S1[B9] holds
S1[B9 \/ {b}]
proof
let B9 be Element of Fin the topology of T; ::_thesis: for b being Element of the topology of T st S1[B9] holds
S1[B9 \/ {b}]
let b be Element of the topology of T; ::_thesis: ( S1[B9] implies S1[B9 \/ {b}] )
A2: meet {b} = b by SETFAM_1:10;
assume A3: meet B9 in the topology of T ; ::_thesis: S1[B9 \/ {b}]
percases ( B9 <> {} or B9 = {} ) ;
suppose B9 <> {} ; ::_thesis: S1[B9 \/ {b}]
then meet (B9 \/ {b}) = (meet B9) /\ (meet {b}) by SETFAM_1:9;
hence S1[B9 \/ {b}] by A2, A3, PRE_TOPC:def_1; ::_thesis: verum
end;
suppose B9 = {} ; ::_thesis: S1[B9 \/ {b}]
hence S1[B9 \/ {b}] by A2; ::_thesis: verum
end;
end;
end;
thus the topology of T c= FinMeetCl the topology of T by Th4; :: according to XBOOLE_0:def_10 ::_thesis: FinMeetCl the topology of T c= the topology of T
A4: S1[ {}. the topology of T] by PRE_TOPC:1, SETFAM_1:1;
A5: for B being Element of Fin the topology of T holds S1[B] from SETWISEO:sch_4(A4, A1);
now__::_thesis:_for_x_being_Subset_of_T_st_x_in_FinMeetCl_the_topology_of_T_holds_
x_in_the_topology_of_T
let x be Subset of T; ::_thesis: ( x in FinMeetCl the topology of T implies b1 in the topology of T )
assume x in FinMeetCl the topology of T ; ::_thesis: b1 in the topology of T
then consider y being Subset-Family of T such that
A6: ( y c= the topology of T & y is finite ) and
A7: x = Intersect y by Def3;
reconsider y = y as Subset-Family of T ;
percases ( y <> {} or y = {} ) ;
supposeA8: y <> {} ; ::_thesis: b1 in the topology of T
A9: y in Fin the topology of T by A6, FINSUB_1:def_5;
x = meet y by A7, A8, SETFAM_1:def_9;
hence x in the topology of T by A5, A9; ::_thesis: verum
end;
supposeA10: y = {} ; ::_thesis: b1 in the topology of T
reconsider aa = {} (bool the carrier of T) as Subset-Family of the carrier of T ;
Intersect aa = the carrier of T by SETFAM_1:def_9;
hence x in the topology of T by A7, A10, PRE_TOPC:def_1; ::_thesis: verum
end;
end;
end;
hence FinMeetCl the topology of T c= the topology of T by SUBSET_1:2; ::_thesis: verum
end;
theorem Th6: :: CANTOR_1:6
for T being TopSpace holds the topology of T = UniCl the topology of T
proof
let T be TopSpace; ::_thesis: the topology of T = UniCl the topology of T
thus the topology of T c= UniCl the topology of T by Th1; :: according to XBOOLE_0:def_10 ::_thesis: UniCl the topology of T c= the topology of T
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in UniCl the topology of T or a in the topology of T )
assume A1: a in UniCl the topology of T ; ::_thesis: a in the topology of T
then reconsider a9 = a as Subset of T ;
ex b being Subset-Family of T st
( b c= the topology of T & a9 = union b ) by A1, Def1;
hence a in the topology of T by PRE_TOPC:def_1; ::_thesis: verum
end;
theorem Th7: :: CANTOR_1:7
for T being non empty TopSpace holds the topology of T = UniCl (FinMeetCl the topology of T)
proof
let T be non empty TopSpace; ::_thesis: the topology of T = UniCl (FinMeetCl the topology of T)
the topology of T = FinMeetCl the topology of T by Th5;
hence the topology of T = UniCl (FinMeetCl the topology of T) by Th6; ::_thesis: verum
end;
theorem Th8: :: CANTOR_1:8
for X being set
for A being Subset-Family of X holds X in FinMeetCl A
proof
let X be set ; ::_thesis: for A being Subset-Family of X holds X in FinMeetCl A
let A be Subset-Family of X; ::_thesis: X in FinMeetCl A
{} is Subset-Family of X by XBOOLE_1:2;
then consider y being Subset-Family of X such that
A1: y = {} ;
( y c= A & Intersect y = X ) by A1, SETFAM_1:def_9, XBOOLE_1:2;
hence X in FinMeetCl A by A1, Def3; ::_thesis: verum
end;
theorem Th9: :: CANTOR_1:9
for X being set
for A, B being Subset-Family of X st A c= B holds
UniCl A c= UniCl B
proof
let X be set ; ::_thesis: for A, B being Subset-Family of X st A c= B holds
UniCl A c= UniCl B
let A, B be Subset-Family of X; ::_thesis: ( A c= B implies UniCl A c= UniCl B )
assume A1: A c= B ; ::_thesis: UniCl A c= UniCl B
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in UniCl A or x in UniCl B )
assume A2: x in UniCl A ; ::_thesis: x in UniCl B
then reconsider x9 = x as Subset of X ;
consider T being Subset-Family of X such that
A3: T c= A and
A4: x9 = union T by A2, Def1;
T c= B by A1, A3, XBOOLE_1:1;
hence x in UniCl B by A4, Def1; ::_thesis: verum
end;
theorem Th10: :: CANTOR_1:10
for X being set
for R being non empty Subset-Family of (bool X)
for F being Subset-Family of X st F = { (Intersect x) where x is Element of R : verum } holds
Intersect F = Intersect (union R)
proof
let X be set ; ::_thesis: for R being non empty Subset-Family of (bool X)
for F being Subset-Family of X st F = { (Intersect x) where x is Element of R : verum } holds
Intersect F = Intersect (union R)
let R be non empty Subset-Family of (bool X); ::_thesis: for F being Subset-Family of X st F = { (Intersect x) where x is Element of R : verum } holds
Intersect F = Intersect (union R)
let F be Subset-Family of X; ::_thesis: ( F = { (Intersect x) where x is Element of R : verum } implies Intersect F = Intersect (union R) )
assume A1: F = { (Intersect x) where x is Element of R : verum } ; ::_thesis: Intersect F = Intersect (union R)
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: Intersect (union R) c= Intersect F
let c be set ; ::_thesis: ( c in Intersect F implies c in Intersect (union R) )
assume A2: c in Intersect F ; ::_thesis: c in Intersect (union R)
for Y being set st Y in union R holds
c in Y
proof
let Y be set ; ::_thesis: ( Y in union R implies c in Y )
assume Y in union R ; ::_thesis: c in Y
then consider d being set such that
A3: Y in d and
A4: d in R by TARSKI:def_4;
reconsider d = d as Subset-Family of X by A4;
reconsider d = d as Subset-Family of X ;
Intersect d in F by A1, A4;
then c in Intersect d by A2, SETFAM_1:43;
hence c in Y by A3, SETFAM_1:43; ::_thesis: verum
end;
hence c in Intersect (union R) by A2, SETFAM_1:43; ::_thesis: verum
end;
let c be set ; :: according to TARSKI:def_3 ::_thesis: ( not c in Intersect (union R) or c in Intersect F )
assume A5: c in Intersect (union R) ; ::_thesis: c in Intersect F
for Y being set st Y in F holds
c in Y
proof
let Y be set ; ::_thesis: ( Y in F implies c in Y )
assume Y in F ; ::_thesis: c in Y
then consider x being Element of R such that
A6: Y = Intersect x by A1;
Intersect (union R) c= Intersect x by SETFAM_1:44, ZFMISC_1:74;
hence c in Y by A5, A6; ::_thesis: verum
end;
hence c in Intersect F by A5, SETFAM_1:43; ::_thesis: verum
end;
theorem Th11: :: CANTOR_1:11
for X being set
for A being Subset-Family of X holds FinMeetCl A = FinMeetCl (FinMeetCl A)
proof
let X be set ; ::_thesis: for A being Subset-Family of X holds FinMeetCl A = FinMeetCl (FinMeetCl A)
let A be Subset-Family of X; ::_thesis: FinMeetCl A = FinMeetCl (FinMeetCl A)
defpred S1[ set , set ] means ex A being Subset-Family of X st
( $1 = Intersect A & A = $2 & $2 is finite );
thus FinMeetCl A c= FinMeetCl (FinMeetCl A) by Th4; :: according to XBOOLE_0:def_10 ::_thesis: FinMeetCl (FinMeetCl A) c= FinMeetCl A
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in FinMeetCl (FinMeetCl A) or x in FinMeetCl A )
assume A1: x in FinMeetCl (FinMeetCl A) ; ::_thesis: x in FinMeetCl A
then reconsider x9 = x as Subset of X ;
consider Y being Subset-Family of X such that
A2: Y c= FinMeetCl A and
A3: Y is finite and
A4: x9 = Intersect Y by A1, Def3;
A5: for e being set st e in Y holds
ex u being set st
( u in bool A & S1[e,u] )
proof
let e be set ; ::_thesis: ( e in Y implies ex u being set st
( u in bool A & S1[e,u] ) )
assume A6: e in Y ; ::_thesis: ex u being set st
( u in bool A & S1[e,u] )
then reconsider e9 = e as Subset of X ;
consider Y being Subset-Family of X such that
A7: ( Y c= A & Y is finite & e9 = Intersect Y ) by A2, A6, Def3;
take Y ; ::_thesis: ( Y in bool A & S1[e,Y] )
thus ( Y in bool A & S1[e,Y] ) by A7; ::_thesis: verum
end;
consider f being Function of Y,(bool A) such that
A8: for e being set st e in Y holds
S1[e,f . e] from FUNCT_2:sch_1(A5);
set fz = { (Intersect s) where s is Subset-Family of X : s in rng f } ;
A9: { (Intersect s) where s is Subset-Family of X : s in rng f } c= Y
proof
let l be set ; :: according to TARSKI:def_3 ::_thesis: ( not l in { (Intersect s) where s is Subset-Family of X : s in rng f } or l in Y )
assume l in { (Intersect s) where s is Subset-Family of X : s in rng f } ; ::_thesis: l in Y
then consider s being Subset-Family of X such that
A10: l = Intersect s and
A11: s in rng f ;
consider v being set such that
A12: v in dom f and
A13: s = f . v by A11, FUNCT_1:def_3;
v in Y by A12, FUNCT_2:def_1;
then S1[v,f . v] by A8;
hence l in Y by A10, A12, A13, FUNCT_2:def_1; ::_thesis: verum
end;
rng f c= bool A by RELAT_1:def_19;
then union (rng f) c= union (bool A) by ZFMISC_1:77;
then A14: union (rng f) c= A by ZFMISC_1:81;
then reconsider y = union (rng f) as Subset-Family of X by XBOOLE_1:1;
reconsider y = y as Subset-Family of X ;
Y c= { (Intersect s) where s is Subset-Family of X : s in rng f }
proof
let l be set ; :: according to TARSKI:def_3 ::_thesis: ( not l in Y or l in { (Intersect s) where s is Subset-Family of X : s in rng f } )
assume A15: l in Y ; ::_thesis: l in { (Intersect s) where s is Subset-Family of X : s in rng f }
then consider C being Subset-Family of X such that
A16: l = Intersect C and
A17: C = f . l and
f . l is finite by A8;
l in dom f by A15, FUNCT_2:def_1;
then C in rng f by A17, FUNCT_1:def_3;
hence l in { (Intersect s) where s is Subset-Family of X : s in rng f } by A16; ::_thesis: verum
end;
then A18: Y = { (Intersect s) where s is Subset-Family of X : s in rng f } by A9, XBOOLE_0:def_10;
A19: x = Intersect y
proof
percases ( rng f <> {} or rng f = {} ) ;
supposeA20: rng f <> {} ; ::_thesis: x = Intersect y
( rng f c= bool A & bool A c= bool (bool X) ) by RELAT_1:def_19, ZFMISC_1:67;
then reconsider GGG = rng f as non empty Subset-Family of (bool X) by A20, XBOOLE_1:1;
reconsider GGG = GGG as non empty Subset-Family of (bool X) ;
{ (Intersect s) where s is Subset-Family of X : s in rng f } = { (Intersect b) where b is Element of GGG : verum }
proof
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: { (Intersect b) where b is Element of GGG : verum } c= { (Intersect s) where s is Subset-Family of X : s in rng f }
let x be set ; ::_thesis: ( x in { (Intersect s) where s is Subset-Family of X : s in rng f } implies x in { (Intersect b) where b is Element of GGG : verum } )
assume x in { (Intersect s) where s is Subset-Family of X : s in rng f } ; ::_thesis: x in { (Intersect b) where b is Element of GGG : verum }
then ex s being Subset-Family of X st
( x = Intersect s & s in rng f ) ;
hence x in { (Intersect b) where b is Element of GGG : verum } ; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (Intersect b) where b is Element of GGG : verum } or x in { (Intersect s) where s is Subset-Family of X : s in rng f } )
assume x in { (Intersect b) where b is Element of GGG : verum } ; ::_thesis: x in { (Intersect s) where s is Subset-Family of X : s in rng f }
then ex s being Element of GGG st x = Intersect s ;
hence x in { (Intersect s) where s is Subset-Family of X : s in rng f } ; ::_thesis: verum
end;
hence x = Intersect y by A4, A18, Th10; ::_thesis: verum
end;
supposeA21: rng f = {} ; ::_thesis: x = Intersect y
Y = dom f by FUNCT_2:def_1;
hence x = Intersect y by A4, A21, RELAT_1:38, RELAT_1:41, ZFMISC_1:2; ::_thesis: verum
end;
end;
end;
for V being set st V in rng f holds
V is finite
proof
let V be set ; ::_thesis: ( V in rng f implies V is finite )
assume V in rng f ; ::_thesis: V is finite
then consider x being set such that
A22: x in dom f and
A23: V = f . x by FUNCT_1:def_3;
x in Y by A22, FUNCT_2:def_1;
then reconsider x = x as Subset of X ;
reconsider G = f . x as Subset-Family of X ;
x in Y by A22, FUNCT_2:def_1;
then S1[x,G] by A8;
hence V is finite by A23; ::_thesis: verum
end;
then union (rng f) is finite by A3, FINSET_1:7;
hence x in FinMeetCl A by A14, A19, Def3; ::_thesis: verum
end;
theorem :: CANTOR_1:12
for X being set
for A being Subset-Family of X
for a, b being set st a in FinMeetCl A & b in FinMeetCl A holds
a /\ b in FinMeetCl A
proof
let X be set ; ::_thesis: for A being Subset-Family of X
for a, b being set st a in FinMeetCl A & b in FinMeetCl A holds
a /\ b in FinMeetCl A
let A be Subset-Family of X; ::_thesis: for a, b being set st a in FinMeetCl A & b in FinMeetCl A holds
a /\ b in FinMeetCl A
let a, b be set ; ::_thesis: ( a in FinMeetCl A & b in FinMeetCl A implies a /\ b in FinMeetCl A )
assume A1: ( a in FinMeetCl A & b in FinMeetCl A ) ; ::_thesis: a /\ b in FinMeetCl A
then reconsider M = {a,b} as Subset-Family of X by ZFMISC_1:32;
reconsider M = M as Subset-Family of X ;
a /\ b = meet M by SETFAM_1:11;
then A2: a /\ b = Intersect M by SETFAM_1:def_9;
M c= FinMeetCl A by A1, ZFMISC_1:32;
then Intersect M in FinMeetCl (FinMeetCl A) by Def3;
hence a /\ b in FinMeetCl A by A2, Th11; ::_thesis: verum
end;
theorem Th13: :: CANTOR_1:13
for X being set
for A being Subset-Family of X
for a, b being set st a c= FinMeetCl A & b c= FinMeetCl A holds
INTERSECTION (a,b) c= FinMeetCl A
proof
let X be set ; ::_thesis: for A being Subset-Family of X
for a, b being set st a c= FinMeetCl A & b c= FinMeetCl A holds
INTERSECTION (a,b) c= FinMeetCl A
let A be Subset-Family of X; ::_thesis: for a, b being set st a c= FinMeetCl A & b c= FinMeetCl A holds
INTERSECTION (a,b) c= FinMeetCl A
let a, b be set ; ::_thesis: ( a c= FinMeetCl A & b c= FinMeetCl A implies INTERSECTION (a,b) c= FinMeetCl A )
assume A1: ( a c= FinMeetCl A & b c= FinMeetCl A ) ; ::_thesis: INTERSECTION (a,b) c= FinMeetCl A
let Z be set ; :: according to TARSKI:def_3 ::_thesis: ( not Z in INTERSECTION (a,b) or Z in FinMeetCl A )
assume Z in INTERSECTION (a,b) ; ::_thesis: Z in FinMeetCl A
then consider V, B being set such that
A2: ( V in a & B in b ) and
A3: Z = V /\ B by SETFAM_1:def_5;
( V in FinMeetCl A & B in FinMeetCl A ) by A1, A2;
then reconsider M = {V,B} as Subset-Family of X by ZFMISC_1:32;
reconsider M = M as Subset-Family of X ;
V /\ B = meet M by SETFAM_1:11;
then A4: V /\ B = Intersect M by SETFAM_1:def_9;
M c= FinMeetCl A by A1, A2, ZFMISC_1:32;
then Intersect M in FinMeetCl (FinMeetCl A) by Def3;
hence Z in FinMeetCl A by A3, A4, Th11; ::_thesis: verum
end;
theorem Th14: :: CANTOR_1:14
for X being set
for A, B being Subset-Family of X st A c= B holds
FinMeetCl A c= FinMeetCl B
proof
let X be set ; ::_thesis: for A, B being Subset-Family of X st A c= B holds
FinMeetCl A c= FinMeetCl B
let A, B be Subset-Family of X; ::_thesis: ( A c= B implies FinMeetCl A c= FinMeetCl B )
assume A1: A c= B ; ::_thesis: FinMeetCl A c= FinMeetCl B
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in FinMeetCl A or x in FinMeetCl B )
assume A2: x in FinMeetCl A ; ::_thesis: x in FinMeetCl B
then reconsider x = x as Subset of X ;
consider y being Subset-Family of X such that
A3: y c= A and
A4: ( y is finite & x = Intersect y ) by A2, Def3;
y c= B by A1, A3, XBOOLE_1:1;
hence x in FinMeetCl B by A4, Def3; ::_thesis: verum
end;
registration
let X be set ;
let A be Subset-Family of X;
cluster FinMeetCl A -> non empty ;
coherence
not FinMeetCl A is empty by Th8;
end;
theorem Th15: :: CANTOR_1:15
for X being non empty set
for A being Subset-Family of X holds TopStruct(# X,(UniCl (FinMeetCl A)) #) is TopSpace-like
proof
let X be non empty set ; ::_thesis: for A being Subset-Family of X holds TopStruct(# X,(UniCl (FinMeetCl A)) #) is TopSpace-like
let A be Subset-Family of X; ::_thesis: TopStruct(# X,(UniCl (FinMeetCl A)) #) is TopSpace-like
set T = TopStruct(# X,(UniCl (FinMeetCl A)) #);
A1: [#] TopStruct(# X,(UniCl (FinMeetCl A)) #) in FinMeetCl A by Th8;
now__::_thesis:_ex_Y_being_Subset-Family_of_X_st_
(_Y_c=_FinMeetCl_A_&_[#]_TopStruct(#_X,(UniCl_(FinMeetCl_A))_#)_=_union_Y_)
reconsider Y = {([#] TopStruct(# X,(UniCl (FinMeetCl A)) #))} as Subset-Family of X by ZFMISC_1:68;
reconsider Y = Y as Subset-Family of X ;
take Y = Y; ::_thesis: ( Y c= FinMeetCl A & [#] TopStruct(# X,(UniCl (FinMeetCl A)) #) = union Y )
thus Y c= FinMeetCl A by A1, ZFMISC_1:31; ::_thesis: [#] TopStruct(# X,(UniCl (FinMeetCl A)) #) = union Y
thus [#] TopStruct(# X,(UniCl (FinMeetCl A)) #) = union Y by ZFMISC_1:25; ::_thesis: verum
end;
hence the carrier of TopStruct(# X,(UniCl (FinMeetCl A)) #) in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) by Def1; :: according to PRE_TOPC:def_1 ::_thesis: ( ( for b1 being Element of bool (bool the carrier of TopStruct(# X,(UniCl (FinMeetCl A)) #)) holds
( not b1 c= the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) or union b1 in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) ) ) & ( for b1, b2 being Element of bool the carrier of TopStruct(# X,(UniCl (FinMeetCl A)) #) holds
( not b1 in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) or not b2 in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) or b1 /\ b2 in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) ) ) )
thus for a being Subset-Family of TopStruct(# X,(UniCl (FinMeetCl A)) #) st a c= the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) holds
union a in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) ::_thesis: for b1, b2 being Element of bool the carrier of TopStruct(# X,(UniCl (FinMeetCl A)) #) holds
( not b1 in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) or not b2 in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) or b1 /\ b2 in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) )
proof
let a be Subset-Family of TopStruct(# X,(UniCl (FinMeetCl A)) #); ::_thesis: ( a c= the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) implies union a in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) )
assume A2: a c= the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) ; ::_thesis: union a in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #)
defpred S1[ set ] means ex c being Subset of TopStruct(# X,(UniCl (FinMeetCl A)) #) st
( c in a & c = union $1 );
consider b being Subset-Family of (FinMeetCl A) such that
A3: for B being Subset of (FinMeetCl A) holds
( B in b iff S1[B] ) from SUBSET_1:sch_3();
A4: a = { (union B) where B is Subset of (FinMeetCl A) : B in b }
proof
set gh = { (union B) where B is Subset of (FinMeetCl A) : B in b } ;
hereby :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis: { (union B) where B is Subset of (FinMeetCl A) : B in b } c= a
let x be set ; ::_thesis: ( x in a implies x in { (union B) where B is Subset of (FinMeetCl A) : B in b } )
assume A5: x in a ; ::_thesis: x in { (union B) where B is Subset of (FinMeetCl A) : B in b }
then reconsider x9 = x as Subset of X ;
consider V being Subset-Family of X such that
A6: V c= FinMeetCl A and
A7: x9 = union V by A2, A5, Def1;
V in b by A3, A5, A6, A7;
hence x in { (union B) where B is Subset of (FinMeetCl A) : B in b } by A7; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (union B) where B is Subset of (FinMeetCl A) : B in b } or x in a )
assume x in { (union B) where B is Subset of (FinMeetCl A) : B in b } ; ::_thesis: x in a
then consider B being Subset of (FinMeetCl A) such that
A8: x = union B and
A9: B in b ;
ex c being Subset of TopStruct(# X,(UniCl (FinMeetCl A)) #) st
( c in a & c = union B ) by A3, A9;
hence x in a by A8; ::_thesis: verum
end;
( union (union b) = union { (union B) where B is Subset of (FinMeetCl A) : B in b } & union b c= bool X ) by EQREL_1:54, XBOOLE_1:1;
hence union a in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) by A4, Def1; ::_thesis: verum
end;
let a, b be Subset of TopStruct(# X,(UniCl (FinMeetCl A)) #); ::_thesis: ( not a in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) or not b in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) or a /\ b in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) )
assume a in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) ; ::_thesis: ( not b in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) or a /\ b in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) )
then consider F being Subset-Family of X such that
A10: F c= FinMeetCl A and
A11: a = union F by Def1;
assume b in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) ; ::_thesis: a /\ b in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #)
then consider G being Subset-Family of X such that
A12: G c= FinMeetCl A and
A13: b = union G by Def1;
A14: union (INTERSECTION (F,G)) = a /\ b by A11, A13, SETFAM_1:28;
A15: INTERSECTION (F,G) c= FinMeetCl A by A10, A12, Th13;
then INTERSECTION (F,G) is Subset-Family of X by XBOOLE_1:1;
hence a /\ b in the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) by A15, A14, Def1; ::_thesis: verum
end;
definition
let X be TopStruct ;
let F be Subset-Family of X;
attrF is quasi_prebasis means :Def4: :: CANTOR_1:def 4
ex G being Basis of X st G c= FinMeetCl F;
end;
:: deftheorem Def4 defines quasi_prebasis CANTOR_1:def_4_:_
for X being TopStruct
for F being Subset-Family of X holds
( F is quasi_prebasis iff ex G being Basis of X st G c= FinMeetCl F );
registration
let X be TopStruct ;
cluster the topology of X -> quasi_prebasis ;
coherence
the topology of X is quasi_prebasis
proof
take the topology of X ; :: according to CANTOR_1:def_4 ::_thesis: the topology of X c= FinMeetCl the topology of X
thus the topology of X c= FinMeetCl the topology of X by Th4; ::_thesis: verum
end;
cluster open quasi_basis -> quasi_prebasis for Element of bool (bool the carrier of X);
coherence
for b1 being Basis of X holds b1 is quasi_prebasis
proof
let F be Basis of X; ::_thesis: F is quasi_prebasis
take F ; :: according to CANTOR_1:def_4 ::_thesis: F c= FinMeetCl F
thus F c= FinMeetCl F by Th4; ::_thesis: verum
end;
cluster open quasi_prebasis for Element of bool (bool the carrier of X);
existence
ex b1 being Subset-Family of X st
( b1 is open & b1 is quasi_prebasis )
proof
take the topology of X ; ::_thesis: ( the topology of X is open & the topology of X is quasi_prebasis )
thus ( the topology of X is open & the topology of X is quasi_prebasis ) ; ::_thesis: verum
end;
end;
definition
let X be TopStruct ;
mode prebasis of X is open quasi_prebasis Subset-Family of X;
end;
theorem Th16: :: CANTOR_1:16
for X being non empty set
for Y being Subset-Family of X holds Y is Basis of TopStruct(# X,(UniCl Y) #)
proof
let X be non empty set ; ::_thesis: for Y being Subset-Family of X holds Y is Basis of TopStruct(# X,(UniCl Y) #)
let Y be Subset-Family of X; ::_thesis: Y is Basis of TopStruct(# X,(UniCl Y) #)
Y c= UniCl Y by Th1;
hence Y is Basis of TopStruct(# X,(UniCl Y) #) by Def2, TOPS_2:64; ::_thesis: verum
end;
theorem Th17: :: CANTOR_1:17
for T1, T2 being non empty strict TopSpace
for P being prebasis of T1 st the carrier of T1 = the carrier of T2 & P is prebasis of T2 holds
T1 = T2
proof
let T1, T2 be non empty strict TopSpace; ::_thesis: for P being prebasis of T1 st the carrier of T1 = the carrier of T2 & P is prebasis of T2 holds
T1 = T2
let P be prebasis of T1; ::_thesis: ( the carrier of T1 = the carrier of T2 & P is prebasis of T2 implies T1 = T2 )
assume that
A1: the carrier of T1 = the carrier of T2 and
A2: P is prebasis of T2 ; ::_thesis: T1 = T2
reconsider P9 = P as prebasis of T2 by A2;
consider B1 being Basis of T1 such that
A3: B1 c= FinMeetCl P by Def4;
P c= the topology of T1 by TOPS_2:64;
then FinMeetCl P c= FinMeetCl the topology of T1 by Th14;
then A4: UniCl (FinMeetCl P) c= UniCl (FinMeetCl the topology of T1) by Th9;
P9 c= the topology of T2 by TOPS_2:64;
then FinMeetCl P9 c= FinMeetCl the topology of T2 by Th14;
then A5: UniCl (FinMeetCl P9) c= UniCl (FinMeetCl the topology of T2) by Th9;
A6: the topology of T1 c= UniCl B1 by Def2;
UniCl B1 c= UniCl (FinMeetCl P) by A3, Th9;
then A7: the topology of T1 c= UniCl (FinMeetCl P) by A6, XBOOLE_1:1;
consider B2 being Basis of T2 such that
A8: B2 c= FinMeetCl P9 by Def4;
A9: the topology of T2 c= UniCl B2 by Def2;
UniCl B2 c= UniCl (FinMeetCl P9) by A8, Th9;
then A10: the topology of T2 c= UniCl (FinMeetCl P9) by A9, XBOOLE_1:1;
the topology of T2 = UniCl (FinMeetCl the topology of T2) by Th7;
then A11: UniCl (FinMeetCl P9) = the topology of T2 by A10, A5, XBOOLE_0:def_10;
the topology of T1 = UniCl (FinMeetCl the topology of T1) by Th7;
hence T1 = T2 by A1, A7, A11, A4, XBOOLE_0:def_10; ::_thesis: verum
end;
theorem Th18: :: CANTOR_1:18
for X being non empty set
for Y being Subset-Family of X holds Y is prebasis of TopStruct(# X,(UniCl (FinMeetCl Y)) #)
proof
let X be non empty set ; ::_thesis: for Y being Subset-Family of X holds Y is prebasis of TopStruct(# X,(UniCl (FinMeetCl Y)) #)
let A be Subset-Family of X; ::_thesis: A is prebasis of TopStruct(# X,(UniCl (FinMeetCl A)) #)
set T = TopStruct(# X,(UniCl (FinMeetCl A)) #);
reconsider A9 = A as Subset-Family of TopStruct(# X,(UniCl (FinMeetCl A)) #) ;
now__::_thesis:_(_A9_is_open_&_A9_is_quasi_prebasis_)
( A9 c= FinMeetCl A & FinMeetCl A c= the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) ) by Th1, Th4;
then A9 c= the topology of TopStruct(# X,(UniCl (FinMeetCl A)) #) by XBOOLE_1:1;
hence A9 is open by TOPS_2:64; ::_thesis: A9 is quasi_prebasis
thus A9 is quasi_prebasis ::_thesis: verum
proof
reconsider B = FinMeetCl A9 as Basis of TopStruct(# X,(UniCl (FinMeetCl A)) #) by Th16;
take B ; :: according to CANTOR_1:def_4 ::_thesis: B c= FinMeetCl A9
thus B c= FinMeetCl A9 ; ::_thesis: verum
end;
end;
hence A is prebasis of TopStruct(# X,(UniCl (FinMeetCl A)) #) ; ::_thesis: verum
end;
definition
func the_Cantor_set -> non empty strict TopSpace means :: CANTOR_1:def 5
( the carrier of it = product (NAT --> {0,1}) & ex P being prebasis of it st
for X being Subset of (product (NAT --> {0,1})) holds
( X in P iff ex N, n being Nat st
for F being Element of product (NAT --> {0,1}) holds
( F in X iff F . N = n ) ) );
existence
ex b1 being non empty strict TopSpace st
( the carrier of b1 = product (NAT --> {0,1}) & ex P being prebasis of b1 st
for X being Subset of (product (NAT --> {0,1})) holds
( X in P iff ex N, n being Nat st
for F being Element of product (NAT --> {0,1}) holds
( F in X iff F . N = n ) ) )
proof
defpred S1[ set ] means ex N, n being Nat st
for F being Element of product (NAT --> {0,1}) holds
( F in $1 iff F . N = n );
consider Y being Subset-Family of (product (NAT --> {0,1})) such that
A1: for y being Subset of (product (NAT --> {0,1})) holds
( y in Y iff S1[y] ) from SUBSET_1:sch_3();
reconsider T = TopStruct(# (product (NAT --> {0,1})),(UniCl (FinMeetCl Y)) #) as non empty strict TopSpace by Th15;
take T ; ::_thesis: ( the carrier of T = product (NAT --> {0,1}) & ex P being prebasis of T st
for X being Subset of (product (NAT --> {0,1})) holds
( X in P iff ex N, n being Nat st
for F being Element of product (NAT --> {0,1}) holds
( F in X iff F . N = n ) ) )
thus the carrier of T = product (NAT --> {0,1}) ; ::_thesis: ex P being prebasis of T st
for X being Subset of (product (NAT --> {0,1})) holds
( X in P iff ex N, n being Nat st
for F being Element of product (NAT --> {0,1}) holds
( F in X iff F . N = n ) )
reconsider Y = Y as prebasis of T by Th18;
take Y ; ::_thesis: for X being Subset of (product (NAT --> {0,1})) holds
( X in Y iff ex N, n being Nat st
for F being Element of product (NAT --> {0,1}) holds
( F in X iff F . N = n ) )
thus for X being Subset of (product (NAT --> {0,1})) holds
( X in Y iff ex N, n being Nat st
for F being Element of product (NAT --> {0,1}) holds
( F in X iff F . N = n ) ) by A1; ::_thesis: verum
end;
uniqueness
for b1, b2 being non empty strict TopSpace st the carrier of b1 = product (NAT --> {0,1}) & ex P being prebasis of b1 st
for X being Subset of (product (NAT --> {0,1})) holds
( X in P iff ex N, n being Nat st
for F being Element of product (NAT --> {0,1}) holds
( F in X iff F . N = n ) ) & the carrier of b2 = product (NAT --> {0,1}) & ex P being prebasis of b2 st
for X being Subset of (product (NAT --> {0,1})) holds
( X in P iff ex N, n being Nat st
for F being Element of product (NAT --> {0,1}) holds
( F in X iff F . N = n ) ) holds
b1 = b2
proof
let T1, T2 be non empty strict TopSpace; ::_thesis: ( the carrier of T1 = product (NAT --> {0,1}) & ex P being prebasis of T1 st
for X being Subset of (product (NAT --> {0,1})) holds
( X in P iff ex N, n being Nat st
for F being Element of product (NAT --> {0,1}) holds
( F in X iff F . N = n ) ) & the carrier of T2 = product (NAT --> {0,1}) & ex P being prebasis of T2 st
for X being Subset of (product (NAT --> {0,1})) holds
( X in P iff ex N, n being Nat st
for F being Element of product (NAT --> {0,1}) holds
( F in X iff F . N = n ) ) implies T1 = T2 )
assume that
A2: the carrier of T1 = product (NAT --> {0,1}) and
A3: ex P being prebasis of T1 st
for X being Subset of (product (NAT --> {0,1})) holds
( X in P iff ex N, n being Nat st
for F being Element of product (NAT --> {0,1}) holds
( F in X iff F . N = n ) ) and
A4: the carrier of T2 = product (NAT --> {0,1}) and
A5: ex P being prebasis of T2 st
for X being Subset of (product (NAT --> {0,1})) holds
( X in P iff ex N, n being Nat st
for F being Element of product (NAT --> {0,1}) holds
( F in X iff F . N = n ) ) ; ::_thesis: T1 = T2
consider P1 being prebasis of T1 such that
A6: for X being Subset of (product (NAT --> {0,1})) holds
( X in P1 iff ex N, n being Nat st
for F being Element of product (NAT --> {0,1}) holds
( F in X iff F . N = n ) ) by A3;
consider P2 being prebasis of T2 such that
A7: for X being Subset of (product (NAT --> {0,1})) holds
( X in P2 iff ex N, n being Nat st
for F being Element of product (NAT --> {0,1}) holds
( F in X iff F . N = n ) ) by A5;
now__::_thesis:_for_x_being_Subset_of_(product_(NAT_-->_{0,1}))_holds_
(_x_in_P1_iff_x_in_P2_)
let x be Subset of (product (NAT --> {0,1})); ::_thesis: ( x in P1 iff x in P2 )
( x in P1 iff ex N, n being Nat st
for F being Element of product (NAT --> {0,1}) holds
( F in x iff F . N = n ) ) by A6;
hence ( x in P1 iff x in P2 ) by A7; ::_thesis: verum
end;
then P1 = P2 by A2, A4, SUBSET_1:3;
hence T1 = T2 by A2, A4, Th17; ::_thesis: verum
end;
end;
:: deftheorem defines the_Cantor_set CANTOR_1:def_5_:_
for b1 being non empty strict TopSpace holds
( b1 = the_Cantor_set iff ( the carrier of b1 = product (NAT --> {0,1}) & ex P being prebasis of b1 st
for X being Subset of (product (NAT --> {0,1})) holds
( X in P iff ex N, n being Nat st
for F being Element of product (NAT --> {0,1}) holds
( F in X iff F . N = n ) ) ) );