:: TOPS_2 semantic presentation

theorem Th1: :: TOPS_2:1

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

theorem Th2: :: TOPS_2:2

canceled;

theorem Th3: :: TOPS_2:3

for b₁ being 1-sorted
for b₂ being Subset-Family of b₁
for b₃ being set st b₃ c= b₂ holds
b₃ is Subset-Family of b₁

proof end;

theorem Th4: :: TOPS_2:4

canceled;

theorem Th5: :: TOPS_2:5

for b₁ being non empty 1-sorted
for b₂ being Subset-Family of b₁ st b₂ is_a_cover_of b₁ holds
b₂ <> {}

proof end;

theorem Th6: :: TOPS_2:6

for b₁ being 1-sorted
for b₂, b₃ being Subset-Family of b₁ holds (union b₂) \ (union b₃) c= union (b₂ \ b₃)

proof end;

theorem Th7: :: TOPS_2:7

canceled;

theorem Th8: :: TOPS_2:8

canceled;

theorem Th9: :: TOPS_2:9

canceled;

theorem Th10: :: TOPS_2:10

for b₁ being set
for b₂ being Subset-Family of b₁ holds
( b₂ <> {} iff COMPLEMENT b₂ <> {} )

proof end;

theorem Th11: :: TOPS_2:11

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

proof end;

theorem Th12: :: TOPS_2:12

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

proof end;

theorem Th13: :: TOPS_2:13

for b₁ being 1-sorted
for b₂ being Subset-Family of b₁ holds
( COMPLEMENT b₂ is finite iff b₂ is finite )

proof end;

definition

let c₁ be TopStruct ;
let c₂ be Subset-Family of c₁;
attr a₂ is open means :Def1: :: TOPS_2:def 1
for b₁ being Subset of a₁ st b₁ in a₂ holds
b₁ is open;
attr a₂ is closed means :Def2: :: TOPS_2:def 2
for b₁ being Subset of a₁ st b₁ in a₂ holds
b₁ is closed;

end;

:: deftheorem Def1 defines open TOPS_2:def 1 :

:: deftheorem Def2 defines closed TOPS_2:def 2 :

theorem Th14: :: TOPS_2:14

canceled;

theorem Th15: :: TOPS_2:15

canceled;

theorem Th16: :: TOPS_2:16

for b₁ being TopStruct
for b₂ being Subset-Family of b₁ holds
( b₂ is closed iff COMPLEMENT b₂ is open )

proof end;

theorem Th17: :: TOPS_2:17

for b₁ being TopStruct
for b₂ being Subset-Family of b₁ holds
( b₂ is open iff COMPLEMENT b₂ is closed )

proof end;

theorem Th18: :: TOPS_2:18

for b₁ being TopStruct
for b₂, b₃ being Subset-Family of b₁ st b₂ c= b₃ & b₃ is open holds
b₂ is open

proof end;

theorem Th19: :: TOPS_2:19

for b₁ being TopStruct
for b₂, b₃ being Subset-Family of b₁ st b₂ c= b₃ & b₃ is closed holds
b₂ is closed

proof end;

theorem Th20: :: TOPS_2:20

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

proof end;

theorem Th21: :: TOPS_2:21

for b₁ being TopStruct
for b₂, b₃ being Subset-Family of b₁ st b₂ is open holds
b₂ /\ b₃ is open

proof end;

theorem Th22: :: TOPS_2:22

for b₁ being TopStruct
for b₂, b₃ being Subset-Family of b₁ st b₂ is open holds
b₂ \ b₃ is open

proof end;

theorem Th23: :: TOPS_2:23

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

proof end;

theorem Th24: :: TOPS_2:24

for b₁ being TopStruct
for b₂, b₃ being Subset-Family of b₁ st b₂ is closed holds
b₂ /\ b₃ is closed

proof end;

theorem Th25: :: TOPS_2:25

for b₁ being TopStruct
for b₂, b₃ being Subset-Family of b₁ st b₂ is closed holds
b₂ \ b₃ is closed

proof end;

theorem Th26: :: TOPS_2:26

for b₁ being TopSpace
for b₂ being Subset-Family of b₁ st b₂ is open holds
union b₂ is open

proof end;

theorem Th27: :: TOPS_2:27

for b₁ being TopSpace
for b₂ being Subset-Family of b₁ st b₂ is open & b₂ is finite holds
meet b₂ is open

proof end;

theorem Th28: :: TOPS_2:28

for b₁ being TopSpace
for b₂ being Subset-Family of b₁ st b₂ is closed & b₂ is finite holds
union b₂ is closed

proof end;

theorem Th29: :: TOPS_2:29

for b₁ being TopSpace
for b₂ being Subset-Family of b₁ st b₂ is closed holds
meet b₂ is closed

proof end;

theorem Th30: :: TOPS_2:30

canceled;

theorem Th31: :: TOPS_2:31

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

proof end;

theorem Th32: :: TOPS_2:32

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

proof end;

theorem Th33: :: TOPS_2:33

for b₁ being TopStruct
for b₂ being Subset of b₁
for b₃ being SubSpace of b₁ st b₂ is open holds
for b₄ being Subset of b₃ st b₄ = b₂ holds
b₄ is open

proof end;

theorem Th34: :: TOPS_2:34

for b₁ being TopStruct
for b₂ being Subset of b₁
for b₃ being SubSpace of b₁ st b₂ is closed holds
for b₄ being Subset of b₃ st b₄ = b₂ holds
b₄ is closed

proof end;

theorem Th35: :: TOPS_2:35

for b₁ being TopStruct
for b₂ being Subset-Family of b₁
for b₃ being SubSpace of b₁ st b₂ is open holds
for b₄ being Subset-Family of b₃ st b₄ = b₂ holds
b₄ is open

proof end;

theorem Th36: :: TOPS_2:36

for b₁ being TopStruct
for b₂ being Subset-Family of b₁
for b₃ being SubSpace of b₁ st b₂ is closed holds
for b₄ being Subset-Family of b₃ st b₄ = b₂ holds
b₄ is closed

proof end;

theorem Th37: :: TOPS_2:37

canceled;

theorem Th38: :: TOPS_2:38

for b₁ being TopStruct
for b₂, b₃ being Subset of b₁ holds b₂ /\ b₃ is Subset of (b₁ | b₃)

proof end;

definition

let c₁ be TopStruct ;
let c₂ be Subset of c₁;
let c₃ be Subset-Family of c₁;
func c₃ | c₂ -> Subset-Family of (a₁ | a₂) means :Def3: :: TOPS_2:def 3
for b₁ being Subset of (a₁ | a₂) holds
( b₁ in a₄ iff ex b₂ being Subset of a₁ st
( b₂ in a₃ & b₂ /\ a₂ = b₁ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def3 defines | TOPS_2:def 3 :

theorem Th39: :: TOPS_2:39

canceled;

theorem Th40: :: TOPS_2:40

for b₁ being TopStruct
for b₂ being Subset of b₁
for b₃, b₄ being Subset-Family of b₁ st b₃ c= b₄ holds
b₃ | b₂ c= b₄ | b₂

proof end;

theorem Th41: :: TOPS_2:41

for b₁ being TopStruct
for b₂, b₃ being Subset of b₁
for b₄ being Subset-Family of b₁ st b₂ in b₄ holds
b₂ /\ b₃ in b₄ | b₃

proof end;

theorem Th42: :: TOPS_2:42

for b₁ being TopStruct
for b₂, b₃ being Subset of b₁
for b₄ being Subset-Family of b₁ st b₂ c= union b₄ holds
b₂ /\ b₃ c= union (b₄ | b₃)

proof end;

theorem Th43: :: TOPS_2:43

for b₁ being TopStruct
for b₂ being Subset of b₁
for b₃ being Subset-Family of b₁ st b₂ c= union b₃ holds
b₂ = union (b₃ | b₂)

proof end;

theorem Th44: :: TOPS_2:44

for b₁ being TopStruct
for b₂ being Subset of b₁
for b₃ being Subset-Family of b₁ holds union (b₃ | b₂) c= union b₃

proof end;

theorem Th45: :: TOPS_2:45

for b₁ being TopStruct
for b₂ being Subset of b₁
for b₃ being Subset-Family of b₁ st b₂ c= union (b₃ | b₂) holds
b₂ c= union b₃

proof end;

theorem Th46: :: TOPS_2:46

for b₁ being TopStruct
for b₂ being Subset of b₁
for b₃ being Subset-Family of b₁ st b₃ is finite holds
b₃ | b₂ is finite

proof end;

theorem Th47: :: TOPS_2:47

for b₁ being TopStruct
for b₂ being Subset of b₁
for b₃ being Subset-Family of b₁ st b₃ is open holds
b₃ | b₂ is open

proof end;

theorem Th48: :: TOPS_2:48

for b₁ being TopStruct
for b₂ being Subset of b₁
for b₃ being Subset-Family of b₁ st b₃ is closed holds
b₃ | b₂ is closed

proof end;

theorem Th49: :: TOPS_2:49

for b₁ being TopStruct
for b₂ being SubSpace of b₁
for b₃ being Subset-Family of b₂ st b₃ is open holds
ex b₄ being Subset-Family of b₁ st
( b₄ is open & ( for b₅ being Subset of b₁ st b₅ = [#] b₂ holds
b₃ = b₄ | b₅ ) )

proof end;

theorem Th50: :: TOPS_2:50

for b₁ being TopStruct
for b₂ being Subset of b₁
for b₃ being Subset-Family of b₁ ex b₄ being Function st
( dom b₄ = b₃ & rng b₄ = b₃ | b₂ & ( for b₅ being set st b₅ in b₃ holds
for b₆ being Subset of b₁ st b₆ = b₅ holds
b₄ . b₅ = b₆ /\ b₂ ) )

proof end;

theorem Th51: :: TOPS_2:51

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

theorem Th52: :: TOPS_2:52

for b₁ being 1-sorted
for b₂ being non empty 1-sorted
for b₃ being Function of b₁,b₂ holds b₃ " ([#] b₂) = [#] b₁

proof end;

theorem Th53: :: TOPS_2:53

canceled;

theorem Th54: :: TOPS_2:54

for b₁ being 1-sorted
for b₂ being non empty 1-sorted
for b₃ being Function of b₁,b₂
for b₄ being Subset-Family of b₂ holds (" b₃) .: b₄ is Subset-Family of b₁

proof end;

theorem Th55: :: TOPS_2:55

for b₁ being TopStruct
for b₂ being non empty TopStruct
for b₃ being Function of b₁,b₂ holds
( b₃ is continuous iff for b₄ being Subset of b₂ st b₄ is open holds
b₃ " b₄ is open )

proof end;

theorem Th56: :: TOPS_2:56

for b₁, b₂ being TopSpace
for b₃ being Function of b₁,b₂ holds
( b₃ is continuous iff for b₄ being Subset of b₂ holds Cl (b₃ " b₄) c= b₃ " (Cl b₄) )

proof end;

theorem Th57: :: TOPS_2:57

for b₁ being TopSpace
for b₂ being non empty TopSpace
for b₃ being Function of b₁,b₂ holds
( b₃ is continuous iff for b₄ being Subset of b₁ holds b₃ .: (Cl b₄) c= Cl (b₃ .: b₄) )

proof end;

theorem Th58: :: TOPS_2:58

for b₁, b₂ being TopStruct
for b₃ being non empty TopStruct
for b₄ being Function of b₁,b₃
for b₅ being Function of b₃,b₂ st b₄ is continuous & b₅ is continuous holds
b₅ * b₄ is continuous

proof end;

theorem Th59: :: TOPS_2:59

for b₁ being TopStruct
for b₂ being non empty TopStruct
for b₃ being Function of b₁,b₂
for b₄ being Subset-Family of b₂ st b₃ is continuous & b₄ is open holds
for b₅ being Subset-Family of b₁ st b₅ = (" b₃) .: b₄ holds
b₅ is open

proof end;

theorem Th60: :: TOPS_2:60

for b₁, b₂ being TopStruct
for b₃ being Function of b₁,b₂
for b₄ being Subset-Family of b₂ st b₃ is continuous & b₄ is closed holds
for b₅ being Subset-Family of b₁ st b₅ = (" b₃) .: b₄ holds
b₅ is closed

proof end;

definition

let c₁, c₂ be 1-sorted ;
let c₃ be Function of c₁,c₂;
assume that
E23: rng c₃ = [#] c₂ and
E24: c₃ is one-to-one ;
func c₃ /" -> Function of a₂,a₁ equals :Def4: :: TOPS_2:def 4
a₃ " ;
coherence by E23, E24, FUNCT_2:31;

end;

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

notation

let c₁, c₂ be 1-sorted ;
let c₃ be Function of c₁,c₂;
synonym c₃ " for c₃ /" ;

end;

theorem Th61: :: TOPS_2:61

canceled;

theorem Th62: :: TOPS_2:62

for b₁ being 1-sorted
for b₂ being non empty 1-sorted
for b₃ being Function of b₁,b₂ st rng b₃ = [#] b₂ & b₃ is one-to-one holds
( dom (b₃ " ) = [#] b₂ & rng (b₃ " ) = [#] b₁ )

proof end;

theorem Th63: :: TOPS_2:63

for b₁, b₂ being 1-sorted
for b₃ being Function of b₁,b₂ st rng b₃ = [#] b₂ & b₃ is one-to-one holds
b₃ " is one-to-one

proof end;

theorem Th64: :: TOPS_2:64

for b₁ being 1-sorted
for b₂ being non empty 1-sorted
for b₃ being Function of b₁,b₂ st rng b₃ = [#] b₂ & b₃ is one-to-one holds
(b₃ " ) " = b₃

proof end;

theorem Th65: :: TOPS_2:65

for b₁, b₂ being 1-sorted
for b₃ being Function of b₁,b₂ st rng b₃ = [#] b₂ & b₃ is one-to-one holds
( (b₃ " ) * b₃ = id (dom b₃) & b₃ * (b₃ " ) = id (rng b₃) )

proof end;

theorem Th66: :: TOPS_2:66

for b₁ being 1-sorted
for b₂, b₃ being non empty 1-sorted
for b₄ being Function of b₁,b₂
for b₅ being Function of b₂,b₃ st dom b₄ = [#] b₁ & rng b₄ = [#] b₂ & b₄ is one-to-one & dom b₅ = [#] b₂ & rng b₅ = [#] b₃ & b₅ is one-to-one holds
(b₅ * b₄) " = (b₄ " ) * (b₅ " )

proof end;

theorem Th67: :: TOPS_2:67

for b₁, b₂ being 1-sorted
for b₃ being Function of b₁,b₂
for b₄ being Subset of b₁ st rng b₃ = [#] b₂ & b₃ is one-to-one holds
b₃ .: b₄ = (b₃ " ) " b₄

proof end;

theorem Th68: :: TOPS_2:68

for b₁, b₂ being 1-sorted
for b₃ being Function of b₁,b₂
for b₄ being Subset of b₂ st rng b₃ = [#] b₂ & b₃ is one-to-one holds
b₃ " b₄ = (b₃ " ) .: b₄

proof end;

definition

let c₁, c₂ be TopStruct ;
let c₃ be Function of c₁,c₂;
attr a₃ is being_homeomorphism means :Def5: :: TOPS_2:def 5
( dom a₃ = [#] a₁ & rng a₃ = [#] a₂ & a₃ is one-to-one & a₃ is continuous & a₃ " is continuous );

end;

:: deftheorem Def5 defines being_homeomorphism TOPS_2:def 5 :

notation

let c₁, c₂ be TopStruct ;
let c₃ be Function of c₁,c₂;
synonym c₃ is_homeomorphism for being_homeomorphism c₃;

end;

theorem Th69: :: TOPS_2:69

canceled;

theorem Th70: :: TOPS_2:70

for b₁ being TopStruct
for b₂ being non empty TopStruct
for b₃ being Function of b₁,b₂ st b₃ is_homeomorphism holds
b₃ " is_homeomorphism

proof end;

theorem Th71: :: TOPS_2:71

for b₁, b₂, b₃ being non empty TopStruct
for b₄ being Function of b₁,b₂
for b₅ being Function of b₂,b₃ st b₄ is_homeomorphism & b₅ is_homeomorphism holds
b₅ * b₄ is_homeomorphism

proof end;

theorem Th72: :: TOPS_2:72

for b₁ being TopStruct
for b₂ being non empty TopStruct
for b₃ being Function of b₁,b₂ holds
( b₃ is_homeomorphism iff ( dom b₃ = [#] b₁ & rng b₃ = [#] b₂ & b₃ is one-to-one & ( for b₄ being Subset of b₁ holds
( b₄ is closed iff b₃ .: b₄ is closed ) ) ) )

proof end;

theorem Th73: :: TOPS_2:73

for b₁ being non empty TopSpace
for b₂ being TopSpace
for b₃ being Function of b₁,b₂ holds
( b₃ is_homeomorphism iff ( dom b₃ = [#] b₁ & rng b₃ = [#] b₂ & b₃ is one-to-one & ( for b₄ being Subset of b₂ holds b₃ " (Cl b₄) = Cl (b₃ " b₄) ) ) )

proof end;

theorem Th74: :: TOPS_2:74

for b₁ being TopSpace
for b₂ being non empty TopSpace
for b₃ being Function of b₁,b₂ holds
( b₃ is_homeomorphism iff ( dom b₃ = [#] b₁ & rng b₃ = [#] b₂ & b₃ is one-to-one & ( for b₄ being Subset of b₁ holds b₃ .: (Cl b₄) = Cl (b₃ .: b₄) ) ) )

proof end;