:: CANTOR_1 semantic presentation

registration

let c₁ be set ;
let c₂ be non empty set ;
cluster a₁ --> a₂ -> non-empty ;
coherence ;

end;

definition

let c₁ be set ;
let c₂ be Subset-Family of c₁;
func UniCl c₂ -> Subset-Family of a₁ means :Def1: :: CANTOR_1:def 1
for b₁ being Subset of a₁ holds
( b₁ in a₃ iff ex b₂ being Subset-Family of a₁ st
( b₂ c= a₂ & b₁ = union b₂ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines UniCl CANTOR_1:def 1 :

definition

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

proof end;

end;

:: deftheorem Def2 defines Basis CANTOR_1:def 2 :

theorem Th1: :: CANTOR_1:1

for b₁ being set
for b₂ being Subset-Family of b₁ holds b₂ c= UniCl b₂

proof end;

theorem Th2: :: CANTOR_1:2

for b₁ being TopStruct holds the topology of b₁ is Basis of b₁

proof end;

theorem Th3: :: CANTOR_1:3

for b₁ being TopStruct holds the topology of b₁ is open

proof end;

definition

let c₁ be set ;
let c₂ be Subset-Family of c₁;
canceled;
func FinMeetCl c₂ -> Subset-Family of a₁ means :Def4: :: CANTOR_1:def 4
for b₁ being Subset of a₁ holds
( b₁ in a₃ iff ex b₂ being Subset-Family of a₁ st
( b₂ c= a₂ & b₂ is finite & b₁ = Intersect b₂ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 CANTOR_1:def 3 :

:: deftheorem Def4 defines FinMeetCl CANTOR_1:def 4 :

theorem Th4: :: CANTOR_1:4

for b₁ being set
for b₂ being Subset-Family of b₁ holds b₂ c= FinMeetCl b₂

proof end;

registration

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

end;

theorem Th5: :: CANTOR_1:5

for b₁ being non empty TopSpace holds the topology of b₁ = FinMeetCl the topology of b₁

proof end;

theorem Th6: :: CANTOR_1:6

for b₁ being TopSpace holds the topology of b₁ = UniCl the topology of b₁

proof end;

theorem Th7: :: CANTOR_1:7

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

proof end;

theorem Th8: :: CANTOR_1:8

for b₁ being set
for b₂ being Subset-Family of b₁ holds b₁ in FinMeetCl b₂

proof end;

theorem Th9: :: CANTOR_1:9

for b₁ being set
for b₂, b₃ being Subset-Family of b₁ st b₂ c= b₃ holds
UniCl b₂ c= UniCl b₃

proof end;

theorem Th10: :: CANTOR_1:10

canceled;

theorem Th11: :: CANTOR_1:11

canceled;

theorem Th12: :: CANTOR_1:12

for b₁ being set
for b₂ being non empty Subset-Family of (bool b₁)
for b₃ being Subset-Family of b₁ st b₃ = { (Intersect b₄) where B is Element of b₂ : verum } holds
Intersect b₃ = Intersect (union b₂)

proof end;

definition

let c₁, c₂ be set ;
let c₃ be Subset-Family of c₁;
let c₄ be Function of c₂, bool c₃;
let c₅ be set ;
redefine func . as c₄ . c₅ -> Subset-Family of a₁;
coherence

proof end;

end;

theorem Th13: :: CANTOR_1:13

for b₁ being set
for b₂ being Subset-Family of b₁ holds FinMeetCl b₂ = FinMeetCl (FinMeetCl b₂)

proof end;

theorem Th14: :: CANTOR_1:14

for b₁ being set
for b₂ being Subset-Family of b₁
for b₃, b₄ being set st b₃ in FinMeetCl b₂ & b₄ in FinMeetCl b₂ holds
b₃ /\ b₄ in FinMeetCl b₂

proof end;

theorem Th15: :: CANTOR_1:15

for b₁ being set
for b₂ being Subset-Family of b₁
for b₃, b₄ being set st b₃ c= FinMeetCl b₂ & b₄ c= FinMeetCl b₂ holds
INTERSECTION b₃,b₄ c= FinMeetCl b₂

proof end;

theorem Th16: :: CANTOR_1:16

for b₁ being set
for b₂, b₃ being Subset-Family of b₁ st b₂ c= b₃ holds
FinMeetCl b₂ c= FinMeetCl b₃

proof end;

registration

let c₁ be set ;
let c₂ be Subset-Family of c₁;
cluster FinMeetCl a₂ -> non empty ;
coherence by Th8;

end;

theorem Th17: :: CANTOR_1:17

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

proof end;

definition

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

proof end;

end;

:: deftheorem Def5 defines prebasis CANTOR_1:def 5 :

theorem Th18: :: CANTOR_1:18

for b₁ being non empty set
for b₂ being Subset-Family of b₁ holds b₂ is Basis of TopStruct(# b₁,(UniCl b₂) #)

proof end;

theorem Th19: :: CANTOR_1:19

for b₁, b₂ being non empty strict TopSpace
for b₃ being prebasis of b₁ st the carrier of b₁ = the carrier of b₂ & b₃ is prebasis of b₂ holds
b₁ = b₂

proof end;

theorem Th20: :: CANTOR_1:20

for b₁ being non empty set
for b₂ being Subset-Family of b₁ holds b₂ is prebasis of TopStruct(# b₁,(UniCl (FinMeetCl b₂)) #)

proof end;

definition

func the_Cantor_set -> non empty strict TopSpace means :: CANTOR_1:def 6
( the carrier of a₁ = product (NAT --> {0,1}) & ex b₁ being prebasis of a₁ st
for b₂ being Subset of (product (NAT --> {0,1})) holds
( b₂ in b₁ iff ex b₃, b₄ being Nat st
for b₅ being Element of product (NAT --> {0,1}) holds
( b₅ in b₂ iff b₅ . b₃ = b₄ ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines the_Cantor_set CANTOR_1:def 6 :