:: PRE_TOPC semantic presentation

definition

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

end;

definition

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

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 S be 1-sorted ;
mode Point of S is Element of S;

end;

theorem :: PRE_TOPC:1

canceled;

theorem :: PRE_TOPC:2

canceled;

theorem :: PRE_TOPC:3

canceled;

theorem :: PRE_TOPC:4

canceled;

theorem Th5: :: PRE_TOPC:5

for GX being TopSpace holds {} in the topology of GX

proof end;

definition

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

proof end;

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

proof end;

end;

:: deftheorem defines {} PRE_TOPC:def 2 :

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

registration

let T be 1-sorted ;
cluster {} T -> empty ;
coherence ;

end;

theorem :: PRE_TOPC:6

canceled;

theorem :: PRE_TOPC:7

canceled;

theorem :: PRE_TOPC:8

canceled;

theorem :: PRE_TOPC:9

canceled;

theorem :: PRE_TOPC:10

canceled;

theorem :: PRE_TOPC:11

canceled;

theorem :: PRE_TOPC:12

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

registration

let T be non empty 1-sorted ;
cluster [#] T -> non empty ;
coherence ;

end;

theorem :: PRE_TOPC:13

for T being non empty 1-sorted
for p being Point of T holds p in [#] T ;

theorem :: PRE_TOPC:14

for T being 1-sorted
for P being Subset of T holds P c= [#] T ;

theorem Th15: :: PRE_TOPC:15

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

theorem :: PRE_TOPC:16

for T being 1-sorted
for A being set st A c= [#] T holds
A is Subset of T ;

theorem Th17: :: PRE_TOPC:17

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

theorem :: PRE_TOPC:18

for T being 1-sorted
for P being Subset of T holds P \/ (P ` ) = [#] T

proof end;

theorem :: PRE_TOPC:19

canceled;

theorem :: PRE_TOPC:20

canceled;

theorem :: PRE_TOPC:21

canceled;

theorem Th22: :: PRE_TOPC:22

for T being 1-sorted
for P being Subset of T holds ([#] T) \ (([#] T) \ P) = P

proof end;

theorem Th23: :: PRE_TOPC:23

for T being 1-sorted
for P being Subset of T holds
( P <> [#] T iff ([#] T) \ P <> {} )

proof end;

theorem :: PRE_TOPC:24

for T being 1-sorted
for P, Q being Subset of T st ([#] T) \ P = Q holds
[#] T = P \/ Q by XBOOLE_1:45;

theorem :: PRE_TOPC:25

for T being 1-sorted
for P, Q being Subset of T st [#] T = P \/ Q & P misses Q holds
Q = ([#] T) \ P

proof end;

theorem :: PRE_TOPC:26

canceled;

theorem :: PRE_TOPC:27

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

proof end;

definition

let T be TopStruct ;
let P be Subset of T;
canceled;
attr P is open means :Def5: :: PRE_TOPC:def 5
P in the topology of T;

end;

:: deftheorem PRE_TOPC:def 4 :

:: deftheorem Def5 defines open PRE_TOPC:def 5 :

definition

let T be TopStruct ;
let P be Subset of T;
attr P is closed means :Def6: :: PRE_TOPC:def 6
([#] T) \ P is open;

end;

:: deftheorem Def6 defines closed PRE_TOPC:def 6 :

definition

let T be 1-sorted ;
let F be Subset-Family of T;
canceled;
pred F is_a_cover_of T means :: PRE_TOPC:def 8
[#] T = union F;

end;

:: deftheorem PRE_TOPC:def 7 :

:: deftheorem defines is_a_cover_of PRE_TOPC:def 8 :

definition

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

proof end;

end;

:: deftheorem Def9 defines SubSpace PRE_TOPC:def 9 :

Lm1: for T being TopStruct holds TopStruct(# the carrier of T,the topology of T #) is SubSpace of T

proof end;

registration

let T be TopStruct ;
cluster strict SubSpace of T;
existence

proof end;

end;

registration

let T be non empty TopStruct ;
cluster non empty strict SubSpace of T;
existence

proof end;

end;

registration

let T be TopSpace;
cluster -> TopSpace-like SubSpace of T;
coherence

proof end;

end;

definition

let T be TopStruct ;
let P be Subset of T;
func T | P -> strict SubSpace of T means :Def10: :: PRE_TOPC:def 10
[#] it = P;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def10 defines | PRE_TOPC:def 10 :

registration

let T be non empty TopStruct ;
let P be non empty Subset of T;
cluster T | P -> non empty strict ;
coherence

proof end;

end;

registration

let T be TopSpace;
cluster strict TopSpace-like SubSpace of T;
existence

proof end;

end;

registration

let T be TopSpace;
let P be Subset of T;
cluster T | P -> strict TopSpace-like ;
coherence ;

end;

definition

let S, T be 1-sorted ;
let f be Function of the carrier of S,the carrier of T;
let P be set ;
:: original: .:
redefine func f .: P -> Subset of T;
coherence

proof end;

end;

definition

let S, T be 1-sorted ;
let f be Function of the carrier of S,the carrier of T;
let P be set ;
:: original: "
redefine func f " P -> Subset of S;
coherence

proof end;

end;

definition

let S, T be TopStruct ;
let f be Function of S,T;
canceled;
attr f is continuous means :: PRE_TOPC:def 12
for P1 being Subset of T st P1 is closed holds
f " P1 is closed;

end;

:: deftheorem PRE_TOPC:def 11 :

:: deftheorem defines continuous PRE_TOPC:def 12 :

theorem :: PRE_TOPC:28

canceled;

theorem :: PRE_TOPC:29

canceled;

theorem :: PRE_TOPC:30

canceled;

theorem :: PRE_TOPC:31

canceled;

theorem :: PRE_TOPC:32

canceled;

theorem :: PRE_TOPC:33

canceled;

theorem :: PRE_TOPC:34

canceled;

theorem :: PRE_TOPC:35

canceled;

theorem :: PRE_TOPC:36

canceled;

theorem :: PRE_TOPC:37

canceled;

theorem :: PRE_TOPC:38

canceled;

theorem Th39: :: PRE_TOPC:39

for T being TopStruct
for X' being SubSpace of T
for A being Subset of X' holds A is Subset of T

proof end;

theorem :: PRE_TOPC:40

canceled;

theorem :: PRE_TOPC:41

for T being TopStruct
for A being Subset of T st A <> {} T holds
ex x being Point of T st x in A

proof end;

theorem Th42: :: PRE_TOPC:42

for GX being TopSpace holds [#] GX is closed

proof end;

registration

let T be TopSpace;
cluster [#] T -> closed ;
coherence by Th42;

end;

registration

let T be TopSpace;
cluster closed Element of bool the carrier of T;
existence

proof end;

end;

registration

let T be non empty TopSpace;
cluster non empty closed Element of bool the carrier of T;
existence

proof end;

end;

theorem Th43: :: PRE_TOPC:43

for T being TopStruct
for X' being SubSpace of T
for B being Subset of X' holds
( B is closed iff ex C being Subset of T st
( C is closed & C /\ ([#] X') = B ) )

proof end;

theorem Th44: :: PRE_TOPC:44

for GX being TopSpace
for F being Subset-Family of GX st ( for A being Subset of GX st A in F holds
A is closed ) holds
meet F is closed

proof end;

definition

let GX be TopStruct ;
let A be Subset of GX;
func Cl A -> Subset of GX means :Def13: :: PRE_TOPC:def 13
for p being set st p in the carrier of GX holds
( p in it iff for G being Subset of GX st G is open & p in G holds
A meets G );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def13 defines Cl PRE_TOPC:def 13 :

theorem Th45: :: PRE_TOPC:45

for T being TopStruct
for A being Subset of T
for p being set st p in the carrier of T holds
( p in Cl A iff for C being Subset of T st C is closed & A c= C holds
p in C )

proof end;

theorem Th46: :: PRE_TOPC:46

for GX being TopSpace
for A being Subset of GX ex F being Subset-Family of GX st
( ( for C being Subset of GX holds
( C in F iff ( C is closed & A c= C ) ) ) & Cl A = meet F )

proof end;

theorem :: PRE_TOPC:47

for T being TopStruct
for X' being SubSpace of T
for A being Subset of T
for A1 being Subset of X' st A = A1 holds
Cl A1 = (Cl A) /\ ([#] X')

proof end;

theorem Th48: :: PRE_TOPC:48

for T being TopStruct
for A being Subset of T holds A c= Cl A

proof end;

theorem Th49: :: PRE_TOPC:49

for T being TopStruct
for A, B being Subset of T st A c= B holds
Cl A c= Cl B

proof end;

theorem :: PRE_TOPC:50

for GX being TopSpace
for A, B being Subset of GX holds Cl (A \/ B) = (Cl A) \/ (Cl B)

proof end;

theorem :: PRE_TOPC:51

for T being TopStruct
for A, B being Subset of T holds Cl (A /\ B) c= (Cl A) /\ (Cl B)

proof end;

theorem Th52: :: PRE_TOPC:52

for T being TopStruct
for A being Subset of T holds
( ( A is closed implies Cl A = A ) & ( T is TopSpace-like & Cl A = A implies A is closed ) )

proof end;

theorem :: PRE_TOPC:53

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

proof end;

theorem :: PRE_TOPC:54

for T being TopStruct
for A being Subset of T
for p being Point of T holds
( p in Cl A iff ( not T is empty & ( for G being Subset of T st G is open & p in G holds
A meets G ) ) )

proof end;