:: COMPTS_1 semantic presentation

definition

let c₁ be 1-sorted ;
let c₂ be Subset-Family of c₁;
let c₃ be Subset of c₁;
pred c₂ is_a_cover_of c₃ means :Def1: :: COMPTS_1:def 1
a₃ c= union a₂;

end;

:: deftheorem Def1 defines is_a_cover_of COMPTS_1:def 1 :

definition

let c₁ be set ;
attr a₁ is centered means :Def2: :: COMPTS_1:def 2
( a₁ <> {} & ( for b₁ being set st b₁ <> {} & b₁ c= a₁ & b₁ is finite holds
meet b₁ <> {} ) );

end;

:: deftheorem Def2 defines centered COMPTS_1:def 2 :

definition

let c₁ be TopStruct ;
attr a₁ is compact means :Def3: :: COMPTS_1:def 3
for b₁ being Subset-Family of a₁ st b₁ is_a_cover_of a₁ & b₁ is open holds
ex b₂ being Subset-Family of a₁ st
( b₂ c= b₁ & b₂ is_a_cover_of a₁ & b₂ is finite );
attr a₁ is being_T2 means :Def4: :: COMPTS_1:def 4
for b₁, b₂ being Point of a₁ st b₁ <> b₂ holds
ex b₃, b₄ being Subset of a₁ st
( b₃ is open & b₄ is open & b₁ in b₃ & b₂ in b₄ & b₃ misses b₄ );
attr a₁ is being_T3 means :: COMPTS_1:def 5
for b₁ being Point of a₁
for b₂ being Subset of a₁ st b₂ <> {} & b₂ is closed & b₁ in b₂ ` holds
ex b₃, b₄ being Subset of a₁ st
( b₃ is open & b₄ is open & b₁ in b₃ & b₂ c= b₄ & b₃ misses b₄ );
attr a₁ is being_T4 means :: COMPTS_1:def 6
for b₁, b₂ being Subset of a₁ st b₁ <> {} & b₂ <> {} & b₁ is closed & b₂ is closed & b₁ misses b₂ holds
ex b₃, b₄ being Subset of a₁ st
( b₃ is open & b₄ is open & b₁ c= b₃ & b₂ c= b₄ & b₃ misses b₄ );

end;

:: deftheorem Def3 defines compact COMPTS_1:def 3 :

:: deftheorem Def4 defines being_T2 COMPTS_1:def 4 :

:: deftheorem Def5 defines being_T3 COMPTS_1:def 5 :

:: deftheorem Def6 defines being_T4 COMPTS_1:def 6 :

notation

let c₁ be TopStruct ;
synonym Hausdorff c₁ for being_T2 c₁;
synonym c₁ is_T2 for being_T2 c₁;
synonym c₁ is_T3 for being_T3 c₁;
synonym c₁ is_T4 for being_T4 c₁;

end;

definition

let c₁ be TopStruct ;
let c₂ be Subset of c₁;
attr a₂ is compact means :Def7: :: COMPTS_1:def 7
for b₁ being Subset-Family of a₁ st b₁ is_a_cover_of a₂ & b₁ is open holds
ex b₂ being Subset-Family of a₁ st
( b₂ c= b₁ & b₂ is_a_cover_of a₂ & b₂ is finite );

end;

:: deftheorem Def7 defines compact COMPTS_1:def 7 :

theorem Th1: :: COMPTS_1:1

canceled;

theorem Th2: :: COMPTS_1:2

canceled;

theorem Th3: :: COMPTS_1:3

canceled;

theorem Th4: :: COMPTS_1:4

canceled;

theorem Th5: :: COMPTS_1:5

canceled;

theorem Th6: :: COMPTS_1:6

canceled;

theorem Th7: :: COMPTS_1:7

canceled;

theorem Th8: :: COMPTS_1:8

canceled;

theorem Th9: :: COMPTS_1:9

for b₁ being TopStruct holds {} b₁ is compact

proof end;

theorem Th10: :: COMPTS_1:10

for b₁ being TopStruct holds
( b₁ is compact iff [#] b₁ is compact )

proof end;

theorem Th11: :: COMPTS_1:11

for b₁ being TopStruct
for b₂ being SubSpace of b₁
for b₃ being Subset of b₁ st b₃ c= [#] b₂ holds
( b₃ is compact iff for b₄ being Subset of b₂ st b₄ = b₃ holds
b₄ is compact )

proof end;

theorem Th12: :: COMPTS_1:12

for b₁ being TopStruct
for b₂ being Subset of b₁ holds
( ( b₂ = {} implies ( b₂ is compact iff b₁ | b₂ is compact ) ) & ( b₁ is TopSpace-like & b₂ <> {} implies ( b₂ is compact iff b₁ | b₂ is compact ) ) )

proof end;

theorem Th13: :: COMPTS_1:13

for b₁ being non empty TopSpace holds
( b₁ is compact iff for b₂ being Subset-Family of b₁ st b₂ is centered & b₂ is closed holds
meet b₂ <> {} )

proof end;

theorem Th14: :: COMPTS_1:14

for b₁ being non empty TopSpace holds
( b₁ is compact iff for b₂ being Subset-Family of b₁ st b₂ <> {} & b₂ is closed & meet b₂ = {} holds
ex b₃ being Subset-Family of b₁ st
( b₃ <> {} & b₃ c= b₂ & b₃ is finite & meet b₃ = {} ) )

proof end;

theorem Th15: :: COMPTS_1:15

for b₁ being TopSpace st b₁ is_T2 holds
for b₂ being Subset of b₁ st b₂ <> {} & b₂ is compact holds
for b₃ being Point of b₁ st b₃ in b₂ ` holds
ex b₄, b₅ being Subset of b₁ st
( b₄ is open & b₅ is open & b₃ in b₄ & b₂ c= b₅ & b₄ misses b₅ )

proof end;

theorem Th16: :: COMPTS_1:16

for b₁ being TopSpace
for b₂ being Subset of b₁ st b₁ is_T2 & b₂ is compact holds
b₂ is closed

proof end;

theorem Th17: :: COMPTS_1:17

for b₁ being TopStruct
for b₂ being Subset of b₁ st b₁ is compact & b₂ is closed holds
b₂ is compact

proof end;

theorem Th18: :: COMPTS_1:18

for b₁ being TopSpace
for b₂, b₃ being Subset of b₁ st b₂ is compact & b₃ c= b₂ & b₃ is closed holds
b₃ is compact

proof end;

theorem Th19: :: COMPTS_1:19

for b₁ being TopStruct
for b₂, b₃ being Subset of b₁ st b₂ is compact & b₃ is compact holds
b₂ \/ b₃ is compact

proof end;

theorem Th20: :: COMPTS_1:20

for b₁ being TopSpace
for b₂, b₃ being Subset of b₁ st b₁ is_T2 & b₂ is compact & b₃ is compact holds
b₂ /\ b₃ is compact

proof end;

theorem Th21: :: COMPTS_1:21

for b₁ being TopSpace st b₁ is_T2 & b₁ is compact holds
b₁ is_T3

proof end;

theorem Th22: :: COMPTS_1:22

for b₁ being TopSpace st b₁ is_T2 & b₁ is compact holds
b₁ is_T4

proof end;

theorem Th23: :: COMPTS_1:23

for b₁ being TopStruct
for b₂ being non empty TopStruct
for b₃ being Function of b₁,b₂ st b₁ is compact & b₃ is continuous & rng b₃ = [#] b₂ holds
b₂ is compact

proof end;

theorem Th24: :: COMPTS_1:24

for b₁ being TopStruct
for b₂ being Subset of b₁
for b₃ being non empty TopStruct
for b₄ being Function of b₁,b₃ st b₄ is continuous & rng b₄ = [#] b₃ & b₂ is compact holds
b₄ .: b₂ is compact

proof end;

theorem Th25: :: COMPTS_1:25

for b₁ being TopSpace
for b₂ being non empty TopSpace
for b₃ being Function of b₁,b₂ st b₁ is compact & b₂ is_T2 & rng b₃ = [#] b₂ & b₃ is continuous holds
for b₄ being Subset of b₁ st b₄ is closed holds
b₃ .: b₄ is closed

proof end;

theorem Th26: :: COMPTS_1:26

for b₁ being TopSpace
for b₂ being non empty TopSpace
for b₃ being Function of b₁,b₂ st b₁ is compact & b₂ is_T2 & dom b₃ = [#] b₁ & rng b₃ = [#] b₂ & b₃ is one-to-one & b₃ is continuous holds
b₃ is being_homeomorphism

proof end;