:: The Cantor Set
:: by Alexander Yu. Shibakov and Andrzej Trybulec
::
:: Received January 9, 1995
:: Copyright (c) 1995-2012 Association of Mizar Users


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 ) )
proofend;
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
proofend;
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
proofend;
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 )
proofend;
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
proofend;

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 ) )
proofend;
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
proofend;
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
proofend;

theorem Th5: :: CANTOR_1:5
for T being non empty TopSpace holds the topology of T = FinMeetCl the topology of T
proofend;

theorem Th6: :: CANTOR_1:6
for T being TopSpace holds the topology of T = UniCl the topology of T
proofend;

theorem Th7: :: CANTOR_1:7
for T being non empty TopSpace holds the topology of T = UniCl (FinMeetCl the topology of T)
proofend;

theorem Th8: :: CANTOR_1:8
for X being set
for A being Subset-Family of X holds X in FinMeetCl A
proofend;

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
proofend;

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)
proofend;

theorem Th11: :: CANTOR_1:11
for X being set
for A being Subset-Family of X holds FinMeetCl A = FinMeetCl (FinMeetCl A)
proofend;

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
proofend;

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
proofend;

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
proofend;

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
proofend;

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
proofend;
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
proofend;
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 )
proofend;
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) #)
proofend;

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
proofend;

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)) #)
proofend;

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 ) ) )
proofend;
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
proofend;
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 ) ) ) );