:: CANTOR_1 semantic presentation

registration

let Y be set ;
let x be non empty set ;
cluster Y --> x -> non-empty ;
coherence ;

end;

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines UniCl CANTOR_1:def 1 :

definition

let X be TopStruct ;
mode Basis of X -> Subset-Family of X means :Def2: :: CANTOR_1:def 2
( it c= the topology of X & the topology of X c= UniCl it );
existence

proof end;

end;

:: deftheorem Def2 defines Basis CANTOR_1:def 2 :

theorem Th1: :: CANTOR_1:1

for X being set
for A being Subset-Family of X holds A c= UniCl A

proof end;

theorem Th2: :: CANTOR_1:2

for S being TopStruct holds the topology of S is Basis of S

proof end;

theorem :: CANTOR_1:3

for S being TopStruct holds the topology of S is open

proof end;

definition

let X be set ;
let A be Subset-Family of X;
canceled;
func FinMeetCl A -> Subset-Family of X means :Def4: :: CANTOR_1:def 4
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

proof end;

uniqueness

proof end;

end;

:: deftheorem CANTOR_1:def 3 :

:: deftheorem Def4 defines FinMeetCl CANTOR_1:def 4 :

theorem Th4: :: CANTOR_1:4

for X being set
for A being Subset-Family of X holds A c= FinMeetCl A

proof end;

registration

let T be non empty TopSpace;
cluster the topology of T -> non empty ;
coherence by PRE_TOPC:def 1;

end;

theorem Th5: :: CANTOR_1:5

for T being non empty TopSpace holds the topology of T = FinMeetCl the topology of T

proof end;

theorem Th6: :: CANTOR_1:6

for T being TopSpace holds the topology of T = UniCl the topology of T

proof end;

theorem Th7: :: CANTOR_1:7

for T being non empty TopSpace holds the topology of T = UniCl (FinMeetCl the topology of T)

proof end;

theorem Th8: :: CANTOR_1:8

for X being set
for A being Subset-Family of X holds X in FinMeetCl A

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

theorem :: CANTOR_1:10

canceled;

theorem :: CANTOR_1:11

canceled;

theorem Th12: :: CANTOR_1:12

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

definition

let X, Y be set ;
let A be Subset-Family of X;
let F be Function of Y, bool A;
let x be set ;
:: original: .
redefine func F . x -> Subset-Family of X;
coherence

proof end;

end;

theorem Th13: :: CANTOR_1:13

for X being set
for A being Subset-Family of X holds FinMeetCl A = FinMeetCl (FinMeetCl A)

proof end;

theorem :: CANTOR_1:14

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

theorem Th15: :: CANTOR_1:15

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

theorem Th16: :: CANTOR_1:16

for X being set
for A, B being Subset-Family of X st A c= B holds
FinMeetCl A c= FinMeetCl B

proof end;

registration

let X be set ;
let A be Subset-Family of X;
cluster FinMeetCl A -> non empty ;
coherence by Th8;

end;

theorem Th17: :: CANTOR_1:17

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

proof end;

definition

let X be TopStruct ;
mode prebasis of X -> Subset-Family of X means :Def5: :: CANTOR_1:def 5
( it c= the topology of X & ex F being Basis of X st F c= FinMeetCl it );
existence

proof end;

end;

:: deftheorem Def5 defines prebasis CANTOR_1:def 5 :

theorem Th18: :: CANTOR_1:18

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

proof end;

theorem Th19: :: CANTOR_1:19

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

theorem Th20: :: CANTOR_1:20

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

proof end;

definition

func the_Cantor_set -> non empty strict TopSpace means :: CANTOR_1:def 6
( 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

proof end;

uniqueness

proof end;

end;

:: deftheorem defines the_Cantor_set CANTOR_1:def 6 :