:: TOPS_2 semantic presentation

theorem :: TOPS_2:1

for T being 1-sorted
for F being Subset-Family of T holds F c= bool ([#] T) ;

theorem :: TOPS_2:2

canceled;

theorem Th3: :: TOPS_2:3

for T being 1-sorted
for F being Subset-Family of T
for X being set st X c= F holds
X is Subset-Family of T

proof end;

theorem :: TOPS_2:4

canceled;

theorem :: TOPS_2:5

for T being non empty 1-sorted
for F being Subset-Family of T st F is_a_cover_of T holds
F <> {}

proof end;

theorem :: TOPS_2:6

for T being 1-sorted
for F, G being Subset-Family of T holds (union F) \ (union G) c= union (F \ G)

proof end;

theorem :: TOPS_2:7

canceled;

theorem :: TOPS_2:8

canceled;

theorem :: TOPS_2:9

canceled;

theorem :: TOPS_2:10

for T being set
for F being Subset-Family of T holds
( F <> {} iff COMPLEMENT F <> {} )

proof end;

theorem Th11: :: TOPS_2:11

for T being set
for F being Subset-Family of T st F <> {} holds
meet (COMPLEMENT F) = (union F) `

proof end;

theorem Th12: :: TOPS_2:12

for T being set
for F being Subset-Family of T st F <> {} holds
union (COMPLEMENT F) = (meet F) `

proof end;

theorem Th13: :: TOPS_2:13

for T being 1-sorted
for F being Subset-Family of T holds
( COMPLEMENT F is finite iff F is finite )

proof end;

definition

let T be TopStruct ;
let F be Subset-Family of T;
attr F is open means :Def1: :: TOPS_2:def 1
for P being Subset of T st P in F holds
P is open;
attr F is closed means :Def2: :: TOPS_2:def 2
for P being Subset of T st P in F holds
P is closed;

end;

:: deftheorem Def1 defines open TOPS_2:def 1 :

:: deftheorem Def2 defines closed TOPS_2:def 2 :

theorem :: TOPS_2:14

canceled;

theorem :: TOPS_2:15

canceled;

theorem Th16: :: TOPS_2:16

for T being TopStruct
for F being Subset-Family of T holds
( F is closed iff COMPLEMENT F is open )

proof end;

theorem :: TOPS_2:17

for T being TopStruct
for F being Subset-Family of T holds
( F is open iff COMPLEMENT F is closed )

proof end;

theorem :: TOPS_2:18

for T being TopStruct
for F, G being Subset-Family of T st F c= G & G is open holds
F is open

proof end;

theorem :: TOPS_2:19

for T being TopStruct
for F, G being Subset-Family of T st F c= G & G is closed holds
F is closed

proof end;

theorem :: TOPS_2:20

for T being TopStruct
for F, G being Subset-Family of T st F is open & G is open holds
F \/ G is open

proof end;

theorem :: TOPS_2:21

for T being TopStruct
for F, G being Subset-Family of T st F is open holds
F /\ G is open

proof end;

theorem :: TOPS_2:22

for T being TopStruct
for F, G being Subset-Family of T st F is open holds
F \ G is open

proof end;

theorem :: TOPS_2:23

for T being TopStruct
for F, G being Subset-Family of T st F is closed & G is closed holds
F \/ G is closed

proof end;

theorem :: TOPS_2:24

for T being TopStruct
for F, G being Subset-Family of T st F is closed holds
F /\ G is closed

proof end;

theorem :: TOPS_2:25

for T being TopStruct
for F, G being Subset-Family of T st F is closed holds
F \ G is closed

proof end;

theorem Th26: :: TOPS_2:26

for GX being TopSpace
for W being Subset-Family of GX st W is open holds
union W is open

proof end;

theorem Th27: :: TOPS_2:27

for GX being TopSpace
for W being Subset-Family of GX st W is open & W is finite holds
meet W is open

proof end;

theorem :: TOPS_2:28

for GX being TopSpace
for W being Subset-Family of GX st W is closed & W is finite holds
union W is closed

proof end;

theorem :: TOPS_2:29

for GX being TopSpace
for W being Subset-Family of GX st W is closed holds
meet W is closed

proof end;

theorem :: TOPS_2:30

canceled;

theorem :: TOPS_2:31

for T being TopStruct
for A being SubSpace of T
for F being Subset-Family of A holds F is Subset-Family of T

proof end;

theorem Th32: :: TOPS_2:32

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

proof end;

theorem Th33: :: TOPS_2:33

for T being TopStruct
for Q being Subset of T
for A being SubSpace of T st Q is open holds
for P being Subset of A st P = Q holds
P is open

proof end;

theorem Th34: :: TOPS_2:34

for T being TopStruct
for Q being Subset of T
for A being SubSpace of T st Q is closed holds
for P being Subset of A st P = Q holds
P is closed

proof end;

theorem :: TOPS_2:35

for T being TopStruct
for F being Subset-Family of T
for A being SubSpace of T st F is open holds
for G being Subset-Family of A st G = F holds
G is open

proof end;

theorem :: TOPS_2:36

for T being TopStruct
for F being Subset-Family of T
for A being SubSpace of T st F is closed holds
for G being Subset-Family of A st G = F holds
G is closed

proof end;

theorem :: TOPS_2:37

canceled;

theorem Th38: :: TOPS_2:38

for T being TopStruct
for M, N being Subset of T holds M /\ N is Subset of (T | N)

proof end;

definition

let T be TopStruct ;
let P be Subset of T;
let F be Subset-Family of T;
func F | P -> Subset-Family of (T | P) means :Def3: :: TOPS_2:def 3
for Q being Subset of (T | P) holds
( Q in it iff ex R being Subset of T st
( R in F & R /\ P = Q ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines | TOPS_2:def 3 :

theorem :: TOPS_2:39

canceled;

theorem :: TOPS_2:40

for T being TopStruct
for M being Subset of T
for F, G being Subset-Family of T st F c= G holds
F | M c= G | M

proof end;

theorem Th41: :: TOPS_2:41

for T being TopStruct
for Q, M being Subset of T
for F being Subset-Family of T st Q in F holds
Q /\ M in F | M

proof end;

theorem :: TOPS_2:42

for T being TopStruct
for Q, M being Subset of T
for F being Subset-Family of T st Q c= union F holds
Q /\ M c= union (F | M)

proof end;

theorem :: TOPS_2:43

for T being TopStruct
for M being Subset of T
for F being Subset-Family of T st M c= union F holds
M = union (F | M)

proof end;

theorem Th44: :: TOPS_2:44

for T being TopStruct
for M being Subset of T
for F being Subset-Family of T holds union (F | M) c= union F

proof end;

theorem :: TOPS_2:45

for T being TopStruct
for M being Subset of T
for F being Subset-Family of T st M c= union (F | M) holds
M c= union F

proof end;

theorem :: TOPS_2:46

for T being TopStruct
for M being Subset of T
for F being Subset-Family of T st F is finite holds
F | M is finite

proof end;

theorem :: TOPS_2:47

for T being TopStruct
for M being Subset of T
for F being Subset-Family of T st F is open holds
F | M is open

proof end;

theorem :: TOPS_2:48

for T being TopStruct
for M being Subset of T
for F being Subset-Family of T st F is closed holds
F | M is closed

proof end;

theorem :: TOPS_2:49

for T being TopStruct
for A being SubSpace of T
for F being Subset-Family of A st F is open holds
ex G being Subset-Family of T st
( G is open & ( for AA being Subset of T st AA = [#] A holds
F = G | AA ) )

proof end;

theorem :: TOPS_2:50

for T being TopStruct
for P being Subset of T
for F being Subset-Family of T ex f being Function st
( dom f = F & rng f = F | P & ( for x being set st x in F holds
for Q being Subset of T st Q = x holds
f . x = Q /\ P ) )

proof end;

theorem Th51: :: TOPS_2:51

for T being 1-sorted
for S being non empty 1-sorted
for f being Function of T,S holds
( dom f = [#] T & rng f c= [#] S ) by FUNCT_2:def 1, RELSET_1:12;

theorem Th52: :: TOPS_2:52

for T being 1-sorted
for S being non empty 1-sorted
for f being Function of T,S holds f " ([#] S) = [#] T

proof end;

theorem :: TOPS_2:53

canceled;

theorem :: TOPS_2:54

for T being 1-sorted
for S being non empty 1-sorted
for f being Function of T,S
for H being Subset-Family of S holds (" f) .: H is Subset-Family of T

proof end;

theorem Th55: :: TOPS_2:55

for T being TopStruct
for S being non empty TopStruct
for f being Function of T,S holds
( f is continuous iff for P1 being Subset of S st P1 is open holds
f " P1 is open )

proof end;

theorem Th56: :: TOPS_2:56

for T, S being TopSpace
for f being Function of T,S holds
( f is continuous iff for P1 being Subset of S holds Cl (f " P1) c= f " (Cl P1) )

proof end;

theorem Th57: :: TOPS_2:57

for T being TopSpace
for S being non empty TopSpace
for f being Function of T,S holds
( f is continuous iff for P being Subset of T holds f .: (Cl P) c= Cl (f .: P) )

proof end;

theorem Th58: :: TOPS_2:58

for T, V being TopStruct
for S being non empty TopStruct
for f being Function of T,S
for g being Function of S,V st f is continuous & g is continuous holds
g * f is continuous

proof end;

theorem :: TOPS_2:59

for T being TopStruct
for S being non empty TopStruct
for f being Function of T,S
for H being Subset-Family of S st f is continuous & H is open holds
for F being Subset-Family of T st F = (" f) .: H holds
F is open

proof end;

theorem :: TOPS_2:60

for T, S being TopStruct
for f being Function of T,S
for H being Subset-Family of S st f is continuous & H is closed holds
for F being Subset-Family of T st F = (" f) .: H holds
F is closed

proof end;

definition

let T, S be 1-sorted ;
let f be Function of T,S;
assume that
A1: rng f = [#] S and
A2: f is one-to-one ;
func f /" -> Function of S,T equals :Def4: :: TOPS_2:def 4
f " ;
coherence by A1, A2, FUNCT_2:31;

end;

:: deftheorem Def4 defines /" TOPS_2:def 4 :

notation

let T, S be 1-sorted ;
let f be Function of T,S;
synonym f " for f /" ;

end;

theorem :: TOPS_2:61

canceled;

theorem Th62: :: TOPS_2:62

for T being 1-sorted
for S being non empty 1-sorted
for f being Function of T,S st rng f = [#] S & f is one-to-one holds
( dom (f " ) = [#] S & rng (f " ) = [#] T )

proof end;

theorem Th63: :: TOPS_2:63

for T, S being 1-sorted
for f being Function of T,S st rng f = [#] S & f is one-to-one holds
f " is one-to-one

proof end;

theorem Th64: :: TOPS_2:64

for T being 1-sorted
for S being non empty 1-sorted
for f being Function of T,S st rng f = [#] S & f is one-to-one holds
(f " ) " = f

proof end;

theorem :: TOPS_2:65

for T, S being 1-sorted
for f being Function of T,S st rng f = [#] S & f is one-to-one holds
( (f " ) * f = id (dom f) & f * (f " ) = id (rng f) )

proof end;

theorem Th66: :: TOPS_2:66

for T being 1-sorted
for S, V being non empty 1-sorted
for f being Function of T,S
for g being Function of S,V st dom f = [#] T & rng f = [#] S & f is one-to-one & dom g = [#] S & rng g = [#] V & g is one-to-one holds
(g * f) " = (f " ) * (g " )

proof end;

theorem Th67: :: TOPS_2:67

for T, S being 1-sorted
for f being Function of T,S
for P being Subset of T st rng f = [#] S & f is one-to-one holds
f .: P = (f " ) " P

proof end;

theorem Th68: :: TOPS_2:68

for T, S being 1-sorted
for f being Function of T,S
for P1 being Subset of S st rng f = [#] S & f is one-to-one holds
f " P1 = (f " ) .: P1

proof end;

definition

let S, T be TopStruct ;
let f be Function of S,T;
attr f is being_homeomorphism means :Def5: :: TOPS_2:def 5
( dom f = [#] S & rng f = [#] T & f is one-to-one & f is continuous & f " is continuous );

end;

:: deftheorem Def5 defines being_homeomorphism TOPS_2:def 5 :

notation

let S, T be TopStruct ;
let f be Function of S,T;
synonym f is_homeomorphism for being_homeomorphism f;

end;

theorem :: TOPS_2:69

canceled;

theorem :: TOPS_2:70

for T being TopStruct
for S being non empty TopStruct
for f being Function of T,S st f is_homeomorphism holds
f " is_homeomorphism

proof end;

theorem :: TOPS_2:71

for T, S, V being non empty TopStruct
for f being Function of T,S
for g being Function of S,V st f is_homeomorphism & g is_homeomorphism holds
g * f is_homeomorphism

proof end;

theorem :: TOPS_2:72

for T being TopStruct
for S being non empty TopStruct
for f being Function of T,S holds
( f is_homeomorphism iff ( dom f = [#] T & rng f = [#] S & f is one-to-one & ( for P being Subset of T holds
( P is closed iff f .: P is closed ) ) ) )

proof end;

theorem :: TOPS_2:73

for T being non empty TopSpace
for S being TopSpace
for f being Function of T,S holds
( f is_homeomorphism iff ( dom f = [#] T & rng f = [#] S & f is one-to-one & ( for P1 being Subset of S holds f " (Cl P1) = Cl (f " P1) ) ) )

proof end;

theorem :: TOPS_2:74

for T being TopSpace
for S being non empty TopSpace
for f being Function of T,S holds
( f is_homeomorphism iff ( dom f = [#] T & rng f = [#] S & f is one-to-one & ( for P being Subset of T holds f .: (Cl P) = Cl (f .: P) ) ) )

proof end;