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

ex b_{1} being Subset-Family of X st

for x being Subset of X holds

( x in b_{1} iff ex Y being Subset-Family of X st

( Y c= A & x = union Y ) )

for b_{1}, b_{2} being Subset-Family of X st ( for x being Subset of X holds

( x in b_{1} iff ex Y being Subset-Family of X st

( Y c= A & x = union Y ) ) ) & ( for x being Subset of X holds

( x in b_{2} iff ex Y being Subset-Family of X st

( Y c= A & x = union Y ) ) ) holds

b_{1} = b_{2}

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

ex b

for x being Subset of X holds

( x in b

( Y c= A & x = union Y ) )

proof end;

uniqueness for b

( x in b

( Y c= A & x = union Y ) ) ) & ( for x being Subset of X holds

( x in b

( Y c= A & x = union Y ) ) ) holds

b

proof end;

:: deftheorem Def1 defines UniCl CANTOR_1:def 1 :

for X being set

for A, b_{3} being Subset-Family of X holds

( b_{3} = UniCl A iff for x being Subset of X holds

( x in b_{3} iff ex Y being Subset-Family of X st

( Y c= A & x = union Y ) ) );

for X being set

for A, b

( b

( x in b

( Y c= A & x = union Y ) ) );

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

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 ;

existence

ex b_{1} being Subset-Family of X st

( b_{1} is open & b_{1} is quasi_basis )

end;
existence

ex b

( b

proof end;

definition

let X be set ;

let A be Subset-Family of X;

ex b_{1} being Subset-Family of X st

for x being Subset of X holds

( x in b_{1} iff ex Y being Subset-Family of X st

( Y c= A & Y is finite & x = Intersect Y ) )

for b_{1}, b_{2} being Subset-Family of X st ( for x being Subset of X holds

( x in b_{1} 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 b_{2} iff ex Y being Subset-Family of X st

( Y c= A & Y is finite & x = Intersect Y ) ) ) holds

b_{1} = b_{2}

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

ex b

for x being Subset of X holds

( x in b

( Y c= A & Y is finite & x = Intersect Y ) )

proof end;

uniqueness for b

( x in b

( Y c= A & Y is finite & x = Intersect Y ) ) ) & ( for x being Subset of X holds

( x in b

( Y c= A & Y is finite & x = Intersect Y ) ) ) holds

b

proof end;

:: deftheorem Def3 defines FinMeetCl CANTOR_1:def 3 :

for X being set

for A, b_{3} being Subset-Family of X holds

( b_{3} = FinMeetCl A iff for x being Subset of X holds

( x in b_{3} iff ex Y being Subset-Family of X st

( Y c= A & Y is finite & x = Intersect Y ) ) );

for X being set

for A, b

( b

( x in b

( Y c= A & Y is finite & x = Intersect Y ) ) );

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)

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

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

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

registration
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

for A being Subset-Family of X holds TopStruct(# X,(UniCl (FinMeetCl A)) #) is TopSpace-like

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

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 ;

coherence

the topology of X is quasi_prebasis

for b_{1} being Basis of X holds b_{1} is quasi_prebasis

ex b_{1} being Subset-Family of X st

( b_{1} is open & b_{1} is quasi_prebasis )

end;
coherence

the topology of X is quasi_prebasis

proof end;

coherence for b

proof end;

existence ex b

( b

proof 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) #)

for Y being Subset-Family of X holds Y is Basis of TopStruct(# X,(UniCl Y) #)

proof 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

for P being prebasis of T1 st the carrier of T1 = the carrier of T2 & P is prebasis of T2 holds

T1 = T2

proof 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)) #)

for Y being Subset-Family of X holds Y is prebasis of TopStruct(# X,(UniCl (FinMeetCl Y)) #)

proof end;

definition

ex b_{1} being non empty strict TopSpace st

( the carrier of b_{1} = product (NAT --> {0,1}) & ex P being prebasis of b_{1} 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 ) ) )

for b_{1}, b_{2} being non empty strict TopSpace st the carrier of b_{1} = product (NAT --> {0,1}) & ex P being prebasis of b_{1} 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 b_{2} = product (NAT --> {0,1}) & ex P being prebasis of b_{2} 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

b_{1} = b_{2}
end;

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

ex b

( the carrier of b

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

uniqueness for b

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 b

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

b

proof end;

:: deftheorem defines the_Cantor_set CANTOR_1:def 5 :

for b_{1} being non empty strict TopSpace holds

( b_{1} = the_Cantor_set iff ( the carrier of b_{1} = product (NAT --> {0,1}) & ex P being prebasis of b_{1} 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 ) ) ) );

for b

( b

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