:: PRE_TOPC semantic presentation

definition

attr a₁ is strict;
struct TopStruct -> 1-sorted ;
aggr TopStruct(# carrier, topology #) -> TopStruct ;
sel topology c₁ -> Subset-Family of the carrier of a₁;

end;

definition

let c₁ be TopStruct ;
attr a₁ is TopSpace-like means :Def1: :: PRE_TOPC:def 1
( the carrier of a₁ in the topology of a₁ & ( for b₁ being Subset-Family of a₁ st b₁ c= the topology of a₁ holds
union b₁ in the topology of a₁ ) & ( for b₁, b₂ being Subset of a₁ st b₁ in the topology of a₁ & b₂ in the topology of a₁ holds
b₁ /\ b₂ in the topology of a₁ ) );

end;

:: deftheorem Def1 defines TopSpace-like PRE_TOPC:def 1 :

registration

cluster non empty strict TopSpace-like TopStruct ;
existence

proof end;

end;

definition

mode TopSpace is TopSpace-like TopStruct ;

end;

definition

let c₁ be 1-sorted ;
mode Point of a₁ is Element of a₁;

end;

theorem Th1: :: PRE_TOPC:1

canceled;

theorem Th2: :: PRE_TOPC:2

canceled;

theorem Th3: :: PRE_TOPC:3

canceled;

theorem Th4: :: PRE_TOPC:4

canceled;

theorem Th5: :: PRE_TOPC:5

for b₁ being TopSpace holds {} in the topology of b₁

proof end;

definition

let c₁ be 1-sorted ;
func {} c₁ -> Subset of a₁ equals :: PRE_TOPC:def 2
{} ;
coherence

proof end;

func [#] c₁ -> Subset of a₁ equals :: PRE_TOPC:def 3
the carrier of a₁;
coherence

proof end;

end;

:: deftheorem Def2 defines {} PRE_TOPC:def 2 :

:: deftheorem Def3 defines [#] PRE_TOPC:def 3 :

registration

let c₁ be 1-sorted ;
cluster {} a₁ -> empty ;
coherence ;

end;

theorem Th6: :: PRE_TOPC:6

canceled;

theorem Th7: :: PRE_TOPC:7

canceled;

theorem Th8: :: PRE_TOPC:8

canceled;

theorem Th9: :: PRE_TOPC:9

canceled;

theorem Th10: :: PRE_TOPC:10

canceled;

theorem Th11: :: PRE_TOPC:11

canceled;

theorem Th12: :: PRE_TOPC:12

for b₁ being 1-sorted holds [#] b₁ = the carrier of b₁ ;

registration

let c₁ be non empty 1-sorted ;
cluster [#] a₁ -> non empty ;
coherence ;

end;

theorem Th13: :: PRE_TOPC:13

for b₁ being non empty 1-sorted
for b₂ being Point of b₁ holds b₂ in [#] b₁ ;

theorem Th14: :: PRE_TOPC:14

for b₁ being 1-sorted
for b₂ being Subset of b₁ holds b₂ c= [#] b₁ ;

theorem Th15: :: PRE_TOPC:15

for b₁ being 1-sorted
for b₂ being Subset of b₁ holds b₂ /\ ([#] b₁) = b₂ by XBOOLE_1:28;

theorem Th16: :: PRE_TOPC:16

for b₁ being 1-sorted
for b₂ being set st b₂ c= [#] b₁ holds
b₂ is Subset of b₁ ;

theorem Th17: :: PRE_TOPC:17

for b₁ being 1-sorted
for b₂ being Subset of b₁ holds b₂ ` = ([#] b₁) \ b₂ by SUBSET_1:def 5;

theorem Th18: :: PRE_TOPC:18

for b₁ being 1-sorted
for b₂ being Subset of b₁ holds b₂ \/ (b₂ ` ) = [#] b₁

proof end;

theorem Th19: :: PRE_TOPC:19

canceled;

theorem Th20: :: PRE_TOPC:20

canceled;

theorem Th21: :: PRE_TOPC:21

canceled;

theorem Th22: :: PRE_TOPC:22

for b₁ being 1-sorted
for b₂ being Subset of b₁ holds ([#] b₁) \ (([#] b₁) \ b₂) = b₂

proof end;

theorem Th23: :: PRE_TOPC:23

for b₁ being 1-sorted
for b₂ being Subset of b₁ holds
( b₂ <> [#] b₁ iff ([#] b₁) \ b₂ <> {} )

proof end;

theorem Th24: :: PRE_TOPC:24

for b₁ being 1-sorted
for b₂, b₃ being Subset of b₁ st ([#] b₁) \ b₂ = b₃ holds
[#] b₁ = b₂ \/ b₃ by XBOOLE_1:45;

theorem Th25: :: PRE_TOPC:25

for b₁ being 1-sorted
for b₂, b₃ being Subset of b₁ st [#] b₁ = b₂ \/ b₃ & b₂ misses b₃ holds
b₃ = ([#] b₁) \ b₂

proof end;

theorem Th26: :: PRE_TOPC:26

canceled;

theorem Th27: :: PRE_TOPC:27

for b₁ being 1-sorted holds [#] b₁ = ({} b₁) `

proof end;

definition

let c₁ be TopStruct ;
let c₂ be Subset of c₁;
canceled;
attr a₂ is open means :Def5: :: PRE_TOPC:def 5
a₂ in the topology of a₁;

end;

:: deftheorem Def4 PRE_TOPC:def 4 :

:: deftheorem Def5 defines open PRE_TOPC:def 5 :

definition

let c₁ be TopStruct ;
let c₂ be Subset of c₁;
attr a₂ is closed means :Def6: :: PRE_TOPC:def 6
([#] a₁) \ a₂ is open;

end;

:: deftheorem Def6 defines closed PRE_TOPC:def 6 :

definition

let c₁ be 1-sorted ;
let c₂ be Subset-Family of c₁;
canceled;
pred c₂ is_a_cover_of c₁ means :: PRE_TOPC:def 8
[#] a₁ = union a₂;

end;

:: deftheorem Def7 PRE_TOPC:def 7 :

:: deftheorem Def8 defines is_a_cover_of PRE_TOPC:def 8 :

definition

let c₁ be TopStruct ;
mode SubSpace of c₁ -> TopStruct means :Def9: :: PRE_TOPC:def 9
( [#] a₂ c= [#] a₁ & ( for b₁ being Subset of a₂ holds
( b₁ in the topology of a₂ iff ex b₂ being Subset of a₁ st
( b₂ in the topology of a₁ & b₁ = b₂ /\ ([#] a₂) ) ) ) );
existence

proof end;

end;

:: deftheorem Def9 defines SubSpace PRE_TOPC:def 9 :

Lemma10: for b₁ being TopStruct holds TopStruct(# the carrier of b₁,the topology of b₁ #) is SubSpace of b₁

proof end;

registration

let c₁ be TopStruct ;
cluster strict SubSpace of a₁;
existence

proof end;

end;

registration

let c₁ be non empty TopStruct ;
cluster non empty strict SubSpace of a₁;
existence

proof end;

end;

registration

let c₁ be TopSpace;
cluster -> TopSpace-like SubSpace of a₁;
coherence

proof end;

end;

definition

let c₁ be TopStruct ;
let c₂ be Subset of c₁;
func c₁ | c₂ -> strict SubSpace of a₁ means :Def10: :: PRE_TOPC:def 10
[#] a₃ = a₂;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def10 defines | PRE_TOPC:def 10 :

registration

let c₁ be non empty TopStruct ;
let c₂ be non empty Subset of c₁;
cluster a₁ | a₂ -> non empty strict ;
coherence

proof end;

end;

registration

let c₁ be TopSpace;
cluster strict TopSpace-like SubSpace of a₁;
existence

proof end;

end;

registration

let c₁ be TopSpace;
let c₂ be Subset of c₁;
cluster a₁ | a₂ -> strict TopSpace-like ;
coherence ;

end;

definition

let c₁, c₂ be 1-sorted ;
let c₃ be Function of the carrier of c₁,the carrier of c₂;
let c₄ be set ;
redefine func .: as c₃ .: c₄ -> Subset of a₂;
coherence

proof end;

end;

definition

let c₁, c₂ be 1-sorted ;
let c₃ be Function of the carrier of c₁,the carrier of c₂;
let c₄ be set ;
redefine func " as c₃ " c₄ -> Subset of a₁;
coherence

proof end;

end;

definition

let c₁, c₂ be TopStruct ;
let c₃ be Function of c₁,c₂;
canceled;
attr a₃ is continuous means :: PRE_TOPC:def 12
for b₁ being Subset of a₂ st b₁ is closed holds
a₃ " b₁ is closed;

end;

:: deftheorem Def11 PRE_TOPC:def 11 :

:: deftheorem Def12 defines continuous PRE_TOPC:def 12 :

theorem Th28: :: PRE_TOPC:28

canceled;

theorem Th29: :: PRE_TOPC:29

canceled;

theorem Th30: :: PRE_TOPC:30

canceled;

theorem Th31: :: PRE_TOPC:31

canceled;

theorem Th32: :: PRE_TOPC:32

canceled;

theorem Th33: :: PRE_TOPC:33

canceled;

theorem Th34: :: PRE_TOPC:34

canceled;

theorem Th35: :: PRE_TOPC:35

canceled;

theorem Th36: :: PRE_TOPC:36

canceled;

theorem Th37: :: PRE_TOPC:37

canceled;

theorem Th38: :: PRE_TOPC:38

canceled;

theorem Th39: :: PRE_TOPC:39

for b₁ being TopStruct
for b₂ being SubSpace of b₁
for b₃ being Subset of b₂ holds b₃ is Subset of b₁

proof end;

theorem Th40: :: PRE_TOPC:40

canceled;

theorem Th41: :: PRE_TOPC:41

for b₁ being TopStruct
for b₂ being Subset of b₁ st b₂ <> {} b₁ holds
ex b₃ being Point of b₁ st b₃ in b₂

proof end;

theorem Th42: :: PRE_TOPC:42

for b₁ being TopSpace holds [#] b₁ is closed

proof end;

registration

let c₁ be TopSpace;
cluster [#] a₁ -> closed ;
coherence by Th42;

end;

registration

let c₁ be TopSpace;
cluster closed Element of bool the carrier of a₁;
existence

proof end;

end;

registration

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

proof end;

end;

theorem Th43: :: PRE_TOPC:43

for b₁ being TopStruct
for b₂ being SubSpace of b₁
for b₃ being Subset of b₂ holds
( b₃ is closed iff ex b₄ being Subset of b₁ st
( b₄ is closed & b₄ /\ ([#] b₂) = b₃ ) )

proof end;

theorem Th44: :: PRE_TOPC:44

for b₁ being TopSpace
for b₂ being Subset-Family of b₁ st ( for b₃ being Subset of b₁ st b₃ in b₂ holds
b₃ is closed ) holds
meet b₂ is closed

proof end;

definition

let c₁ be TopStruct ;
let c₂ be Subset of c₁;
func Cl c₂ -> Subset of a₁ means :Def13: :: PRE_TOPC:def 13
for b₁ being set st b₁ in the carrier of a₁ holds
( b₁ in a₃ iff for b₂ being Subset of a₁ st b₂ is open & b₁ in b₂ holds
a₂ meets b₂ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def13 defines Cl PRE_TOPC:def 13 :

theorem Th45: :: PRE_TOPC:45

for b₁ being TopStruct
for b₂ being Subset of b₁
for b₃ being set st b₃ in the carrier of b₁ holds
( b₃ in Cl b₂ iff for b₄ being Subset of b₁ st b₄ is closed & b₂ c= b₄ holds
b₃ in b₄ )

proof end;

theorem Th46: :: PRE_TOPC:46

for b₁ being TopSpace
for b₂ being Subset of b₁ ex b₃ being Subset-Family of b₁ st
( ( for b₄ being Subset of b₁ holds
( b₄ in b₃ iff ( b₄ is closed & b₂ c= b₄ ) ) ) & Cl b₂ = meet b₃ )

proof end;

theorem Th47: :: PRE_TOPC:47

for b₁ being TopStruct
for b₂ being SubSpace of b₁
for b₃ being Subset of b₁
for b₄ being Subset of b₂ st b₃ = b₄ holds
Cl b₄ = (Cl b₃) /\ ([#] b₂)

proof end;

theorem Th48: :: PRE_TOPC:48

for b₁ being TopStruct
for b₂ being Subset of b₁ holds b₂ c= Cl b₂

proof end;

theorem Th49: :: PRE_TOPC:49

for b₁ being TopStruct
for b₂, b₃ being Subset of b₁ st b₂ c= b₃ holds
Cl b₂ c= Cl b₃

proof end;

theorem Th50: :: PRE_TOPC:50

for b₁ being TopSpace
for b₂, b₃ being Subset of b₁ holds Cl (b₂ \/ b₃) = (Cl b₂) \/ (Cl b₃)

proof end;

theorem Th51: :: PRE_TOPC:51

for b₁ being TopStruct
for b₂, b₃ being Subset of b₁ holds Cl (b₂ /\ b₃) c= (Cl b₂) /\ (Cl b₃)

proof end;

theorem Th52: :: PRE_TOPC:52

for b₁ being TopStruct
for b₂ being Subset of b₁ holds
( ( b₂ is closed implies Cl b₂ = b₂ ) & ( b₁ is TopSpace-like & Cl b₂ = b₂ implies b₂ is closed ) )

proof end;

theorem Th53: :: PRE_TOPC:53

for b₁ being TopStruct
for b₂ being Subset of b₁ holds
( ( b₂ is open implies Cl (([#] b₁) \ b₂) = ([#] b₁) \ b₂ ) & ( b₁ is TopSpace-like & Cl (([#] b₁) \ b₂) = ([#] b₁) \ b₂ implies b₂ is open ) )

proof end;

theorem Th54: :: PRE_TOPC:54

for b₁ being TopStruct
for b₂ being Subset of b₁
for b₃ being Point of b₁ holds
( b₃ in Cl b₂ iff ( not b₁ is empty & ( for b₄ being Subset of b₁ st b₄ is open & b₃ in b₄ holds
b₂ meets b₄ ) ) )

proof end;