:: YELLOW_8 semantic presentation

theorem Th1: :: YELLOW_8:1

for b₁, b₂, b₃ being set st b₂ in Fin b₁ & b₃ c= b₂ holds
b₃ in Fin b₁

proof end;

theorem Th2: :: YELLOW_8:2

for b₁ being set
for b₂ being Subset-Family of b₁ st b₂ c= Fin b₁ holds
meet b₂ in Fin b₁

proof end;

definition

let c₁ be non empty set ;
redefine attr a₁ is trivial means :Def1: :: YELLOW_8:def 1
for b₁, b₂ being Element of a₁ holds b₁ = b₂;
compatibility

proof end;

end;

:: deftheorem Def1 defines trivial YELLOW_8:def 1 :

theorem Th3: :: YELLOW_8:3

canceled;

theorem Th4: :: YELLOW_8:4

for b₁ being set
for b₂ being Subset-Family of b₁ holds b₂, COMPLEMENT b₂ are_equipotent

proof end;

theorem Th5: :: YELLOW_8:5

for b₁, b₂ being set st b₁,b₂ are_equipotent & b₁ is countable holds
b₂ is countable

proof end;

theorem Th6: :: YELLOW_8:6

canceled;

theorem Th7: :: YELLOW_8:7

canceled;

theorem Th8: :: YELLOW_8:8

canceled;

theorem Th9: :: YELLOW_8:9

canceled;

theorem Th10: :: YELLOW_8:10

canceled;

theorem Th11: :: YELLOW_8:11

canceled;

theorem Th12: :: YELLOW_8:12

canceled;

theorem Th13: :: YELLOW_8:13

canceled;

theorem Th14: :: YELLOW_8:14

for b₁ being 1-sorted
for b₂ being Subset-Family of b₁
for b₃ being Subset of b₁ holds
( b₃ ` in COMPLEMENT b₂ iff b₃ in b₂ )

proof end;

theorem Th15: :: YELLOW_8:15

for b₁ being 1-sorted
for b₂ being Subset-Family of b₁ holds Intersect (COMPLEMENT b₂) = (union b₂) `

proof end;

theorem Th16: :: YELLOW_8:16

for b₁ being 1-sorted
for b₂ being Subset-Family of b₁ holds union (COMPLEMENT b₂) = (Intersect b₂) `

proof end;

theorem Th17: :: YELLOW_8:17

for b₁ being non empty TopSpace
for b₂, b₃ being Subset of b₁ st b₃ c= b₂ & b₂ is closed & ( for b₄ being Subset of b₁ st b₃ c= b₄ & b₄ is closed holds
b₂ c= b₄ ) holds
b₂ = Cl b₃

proof end;

theorem Th18: :: YELLOW_8:18

for b₁ being TopStruct
for b₂ being Basis of b₁
for b₃ being Subset of b₁ st b₃ is open holds
b₃ = union { b₄ where B is Subset of b₁ : ( b₄ in b₂ & b₄ c= b₃ ) }

proof end;

theorem Th19: :: YELLOW_8:19

for b₁ being TopStruct
for b₂ being Basis of b₁
for b₃ being Subset of b₁ st b₃ in b₂ holds
b₃ is open

proof end;

theorem Th20: :: YELLOW_8:20

for b₁ being non empty TopSpace
for b₂ being Basis of b₁
for b₃ being Subset of b₁ holds Int b₃ = union { b₄ where B is Subset of b₁ : ( b₄ in b₂ & b₄ c= b₃ ) }

proof end;

definition

let c₁ be non empty TopStruct ;
let c₂ be Point of c₁;
mode Basis of c₂ -> Subset-Family of a₁ means :Def2: :: YELLOW_8:def 2
( a₃ c= the topology of a₁ & a₂ in Intersect a₃ & ( for b₁ being Subset of a₁ st b₁ is open & a₂ in b₁ holds
ex b₂ being Subset of a₁ st
( b₂ in a₃ & b₂ c= b₁ ) ) );
existence

proof end;

end;

:: deftheorem Def2 defines Basis YELLOW_8:def 2 :

theorem Th21: :: YELLOW_8:21

for b₁ being non empty TopStruct
for b₂ being Point of b₁
for b₃ being Basis of b₂
for b₄ being Subset of b₁ st b₄ in b₃ holds
( b₄ is open & b₂ in b₄ )

proof end;

theorem Th22: :: YELLOW_8:22

for b₁ being non empty TopStruct
for b₂ being Point of b₁
for b₃ being Basis of b₂
for b₄ being Subset of b₁ st b₂ in b₄ & b₄ is open holds
ex b₅ being Subset of b₁ st
( b₅ in b₃ & b₅ c= b₄ ) by Def2;

theorem Th23: :: YELLOW_8:23

for b₁ being non empty TopStruct
for b₂ being Subset-Family of b₁ st b₂ c= the topology of b₁ & ( for b₃ being Point of b₁ ex b₄ being Basis of b₃ st b₄ c= b₂ ) holds
b₂ is Basis of b₁

proof end;

definition

let c₁ be non empty TopSpace;
attr a₁ is Baire means :Def3: :: YELLOW_8:def 3
for b₁ being Subset-Family of a₁ st b₁ is countable & ( for b₂ being Subset of a₁ st b₂ in b₁ holds
b₂ is everywhere_dense ) holds
ex b₂ being Subset of a₁ st
( b₂ = Intersect b₁ & b₂ is dense );

end;

:: deftheorem Def3 defines Baire YELLOW_8:def 3 :

theorem Th24: :: YELLOW_8:24

for b₁ being non empty TopSpace holds
( b₁ is Baire iff for b₂ being Subset-Family of b₁ st b₂ is countable & ( for b₃ being Subset of b₁ st b₃ in b₂ holds
b₃ is nowhere_dense ) holds
union b₂ is boundary )

proof end;

definition

let c₁ be TopStruct ;
let c₂ be Subset of c₁;
attr a₂ is irreducible means :Def4: :: YELLOW_8:def 4
( not a₂ is empty & a₂ is closed & ( for b₁, b₂ being Subset of a₁ st b₁ is closed & b₂ is closed & a₂ = b₁ \/ b₂ & not b₁ = a₂ holds
b₂ = a₂ ) );

end;

:: deftheorem Def4 defines irreducible YELLOW_8:def 4 :

registration

let c₁ be TopStruct ;
cluster irreducible -> non empty Element of bool the carrier of a₁;
coherence by Def4;

end;

definition

let c₁ be non empty TopSpace;
let c₂ be Subset of c₁;
let c₃ be Point of c₁;
pred c₃ is_dense_point_of c₂ means :Def5: :: YELLOW_8:def 5
( a₃ in a₂ & a₂ c= Cl {a₃} );

end;

:: deftheorem Def5 defines is_dense_point_of YELLOW_8:def 5 :

theorem Th25: :: YELLOW_8:25

for b₁ being non empty TopSpace
for b₂ being Subset of b₁ st b₂ is closed holds
for b₃ being Point of b₁ st b₃ is_dense_point_of b₂ holds
b₂ = Cl {b₃}

proof end;

theorem Th26: :: YELLOW_8:26

for b₁ being non empty TopSpace
for b₂ being Point of b₁ holds Cl {b₂} is irreducible

proof end;

registration

let c₁ be non empty TopSpace;
cluster non empty irreducible Element of bool the carrier of a₁;
existence

proof end;

end;

definition

let c₁ be non empty TopSpace;
attr a₁ is sober means :Def6: :: YELLOW_8:def 6
for b₁ being irreducible Subset of a₁ ex b₂ being Point of a₁ st
( b₂ is_dense_point_of b₁ & ( for b₃ being Point of a₁ st b₃ is_dense_point_of b₁ holds
b₂ = b₃ ) );

end;

:: deftheorem Def6 defines sober YELLOW_8:def 6 :

theorem Th27: :: YELLOW_8:27

for b₁ being non empty TopSpace
for b₂ being Point of b₁ holds b₂ is_dense_point_of Cl {b₂}

proof end;

theorem Th28: :: YELLOW_8:28

for b₁ being non empty TopSpace
for b₂ being Point of b₁ holds b₂ is_dense_point_of {b₂}

proof end;

theorem Th29: :: YELLOW_8:29

for b₁ being non empty TopSpace
for b₂, b₃ being Subset of b₁ st b₂ is open & b₃ is closed holds
b₃ \ b₂ is closed

proof end;

theorem Th30: :: YELLOW_8:30

for b₁ being non empty Hausdorff TopSpace
for b₂ being irreducible Subset of b₁ holds b₂ is trivial

proof end;

registration

let c₁ be non empty Hausdorff TopSpace;
cluster irreducible -> trivial Element of bool the carrier of a₁;
coherence by Th30;

end;

theorem Th31: :: YELLOW_8:31

for b₁ being non empty Hausdorff TopSpace holds b₁ is sober

proof end;

registration

cluster non empty Hausdorff -> non empty sober TopStruct ;
coherence by Th31;

end;

registration

cluster non empty sober TopStruct ;
existence

proof end;

end;

theorem Th32: :: YELLOW_8:32

for b₁ being non empty TopSpace holds
( b₁ is T_0 iff for b₂, b₃ being Point of b₁ st Cl {b₂} = Cl {b₃} holds
b₂ = b₃ )

proof end;

theorem Th33: :: YELLOW_8:33

for b₁ being non empty sober TopSpace holds b₁ is T_0

proof end;

registration

cluster non empty sober -> non empty T_0 TopStruct ;
coherence by Th33;

end;

definition

let c₁ be set ;
func CofinTop c₁ -> strict TopStruct means :Def7: :: YELLOW_8:def 7
( the carrier of a₂ = a₁ & COMPLEMENT the topology of a₂ = {a₁} \/ (Fin a₁) );
existence

proof end;

uniqueness by SETFAM_1:53;

end;

:: deftheorem Def7 defines CofinTop YELLOW_8:def 7 :

registration

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

proof end;

end;

registration

let c₁ be set ;
cluster CofinTop a₁ -> strict TopSpace-like ;
coherence

proof end;

end;

theorem Th34: :: YELLOW_8:34

for b₁ being non empty set
for b₂ being Subset of (CofinTop b₁) holds
( b₂ is closed iff ( b₂ = b₁ or b₂ is finite ) )

proof end;

theorem Th35: :: YELLOW_8:35

for b₁ being non empty TopSpace st b₁ is_T1 holds
for b₂ being Point of b₁ holds Cl {b₂} = {b₂}

proof end;

registration

let c₁ be non empty set ;
cluster CofinTop a₁ -> non empty strict TopSpace-like being_T1 ;
coherence

proof end;

end;

registration

let c₁ be infinite set ;
cluster CofinTop a₁ -> non empty strict TopSpace-like being_T1 non sober ;
coherence

proof end;

end;

registration

cluster non empty being_T1 non sober TopStruct ;
existence

proof end;

end;

theorem Th36: :: YELLOW_8:36

for b₁ being non empty TopSpace holds
( b₁ is_T3 iff for b₂ being Point of b₁
for b₃ being Subset of b₁ st b₂ in Int b₃ holds
ex b₄ being Subset of b₁ st
( b₄ is closed & b₄ c= b₃ & b₂ in Int b₄ ) )

proof end;

theorem Th37: :: YELLOW_8:37

for b₁ being non empty TopSpace st b₁ is_T3 holds
( b₁ is locally-compact iff for b₂ being Point of b₁ ex b₃ being Subset of b₁ st
( b₂ in Int b₃ & b₃ is compact ) )

proof end;