begin
:: deftheorem Def1 defines UniCl CANTOR_1:def 1 :
:: deftheorem Def2 defines quasi_basis CANTOR_1:def 2 :
theorem Th1:
theorem
theorem
:: deftheorem CANTOR_1:def 3 :
canceled;
:: deftheorem Def4 defines FinMeetCl CANTOR_1:def 4 :
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
theorem
canceled;
theorem
canceled;
theorem Th12:
theorem Th13:
theorem
theorem Th15:
theorem Th16:
theorem Th17:
:: deftheorem Def5 defines quasi_prebasis CANTOR_1:def 5 :
theorem Th18:
theorem Th19:
theorem Th20:
definition
func the_Cantor_set -> non
empty strict TopSpace means
( 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 ) ) )
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
end;
:: deftheorem defines the_Cantor_set CANTOR_1:def 6 :