:: BORSUK_1 semantic presentation

theorem Th1: :: BORSUK_1:1

canceled;

theorem Th2: :: BORSUK_1:2

canceled;

theorem Th3: :: BORSUK_1:3

canceled;

theorem Th4: :: BORSUK_1:4

for b₁ being set
for b₂ being Subset of b₁ holds (id b₁) " b₂ = b₂

proof end;

theorem Th5: :: BORSUK_1:5

for b₁, b₂ being set
for b₃ being Function st b₁ c= b₃ " b₂ holds
b₃ .: b₁ c= b₂

proof end;

theorem Th6: :: BORSUK_1:6

for b₁, b₂, b₃ being set holds (b₁ --> b₂) .: b₃ c= {b₂}

proof end;

theorem Th7: :: BORSUK_1:7

canceled;

theorem Th8: :: BORSUK_1:8

canceled;

theorem Th9: :: BORSUK_1:9

for b₁, b₂, b₃ being set st b₁ c= [:b₂,b₃:] holds
(.: (pr1 b₂,b₃)) . b₁ = (pr1 b₂,b₃) .: b₁

proof end;

theorem Th10: :: BORSUK_1:10

for b₁, b₂, b₃ being set st b₁ c= [:b₂,b₃:] holds
(.: (pr2 b₂,b₃)) . b₁ = (pr2 b₂,b₃) .: b₁

proof end;

theorem Th11: :: BORSUK_1:11

canceled;

theorem Th12: :: BORSUK_1:12

for b₁, b₂ being set
for b₃ being Subset of b₁
for b₄ being Subset of b₂ st [:b₃,b₄:] <> {} holds
( (pr1 b₁,b₂) .: [:b₃,b₄:] = b₃ & (pr2 b₁,b₂) .: [:b₃,b₄:] = b₄ )

proof end;

theorem Th13: :: BORSUK_1:13

for b₁, b₂ being set
for b₃ being Subset of b₁
for b₄ being Subset of b₂ st [:b₃,b₄:] <> {} holds
( (.: (pr1 b₁,b₂)) . [:b₃,b₄:] = b₃ & (.: (pr2 b₁,b₂)) . [:b₃,b₄:] = b₄ )

proof end;

theorem Th14: :: BORSUK_1:14

for b₁, b₂ being set
for b₃ being Subset of [:b₁,b₂:]
for b₄ being Subset-Family of [:b₁,b₂:] st ( for b₅ being set st b₅ in b₄ holds
( b₅ c= b₃ & ex b₆ being Subset of b₁ex b₇ being Subset of b₂ st b₅ = [:b₆,b₇:] ) ) holds
[:(union ((.: (pr1 b₁,b₂)) .: b₄)),(meet ((.: (pr2 b₁,b₂)) .: b₄)):] c= b₃

proof end;

theorem Th15: :: BORSUK_1:15

for b₁, b₂ being set
for b₃ being Subset of [:b₁,b₂:]
for b₄ being Subset-Family of [:b₁,b₂:] st ( for b₅ being set st b₅ in b₄ holds
( b₅ c= b₃ & ex b₆ being Subset of b₁ex b₇ being Subset of b₂ st b₅ = [:b₆,b₇:] ) ) holds
[:(meet ((.: (pr1 b₁,b₂)) .: b₄)),(union ((.: (pr2 b₁,b₂)) .: b₄)):] c= b₃

proof end;

theorem Th16: :: BORSUK_1:16

for b₁ being set
for b₂ being non empty set
for b₃ being Function of b₁,b₂
for b₄ being Subset-Family of b₁ holds union ((.: b₃) .: b₄) = b₃ .: (union b₄)

proof end;

theorem Th17: :: BORSUK_1:17

for b₁ being set
for b₂ being Subset-Family of b₁ holds union (union b₂) = union { (union b₃) where B is Subset of b₁ : b₃ in b₂ }

proof end;

theorem Th18: :: BORSUK_1:18

for b₁ being set
for b₂ being Subset-Family of b₁ st union b₂ = b₁ holds
for b₃ being Subset of b₂
for b₄ being Subset of b₁ st b₄ = union b₃ holds
b₄ ` c= union (b₃ ` )

proof end;

theorem Th19: :: BORSUK_1:19

for b₁, b₂, b₃ being non empty set
for b₄ being Function of b₁,b₂
for b₅ being Function of b₁,b₃ st ( for b₆, b₇ being Element of b₁ st b₄ . b₆ = b₄ . b₇ holds
b₅ . b₆ = b₅ . b₇ ) holds
ex b₆ being Function of b₂,b₃ st b₆ * b₄ = b₅

proof end;

theorem Th20: :: BORSUK_1:20

for b₁, b₂, b₃ being non empty set
for b₄ being Element of b₂
for b₅ being Function of b₁,b₂
for b₆ being Function of b₂,b₃ holds b₅ " {b₄} c= (b₆ * b₅) " {(b₆ . b₄)}

proof end;

theorem Th21: :: BORSUK_1:21

for b₁, b₂, b₃ being non empty set
for b₄ being Function of b₁,b₂
for b₅ being Element of b₁
for b₆ being Element of b₃ holds [:b₄,(id b₃):] . [b₅,b₆] = [(b₄ . b₅),b₆]

proof end;

theorem Th22: :: BORSUK_1:22

canceled;

theorem Th23: :: BORSUK_1:23

for b₁, b₂, b₃ being non empty set
for b₄ being Function of b₁,b₂
for b₅ being Subset of b₁
for b₆ being Subset of b₃ holds [:b₄,(id b₃):] .: [:b₅,b₆:] = [:(b₄ .: b₅),b₆:]

proof end;

theorem Th24: :: BORSUK_1:24

for b₁, b₂, b₃ being non empty set
for b₄ being Function of b₁,b₂
for b₅ being Element of b₂
for b₆ being Element of b₃ holds [:b₄,(id b₃):] " {[b₅,b₆]} = [:(b₄ " {b₅}),{b₆}:]

proof end;

definition

let c₁ be non empty set ;
let c₂ be set ;
let c₃ be Element of c₁;
redefine func --> as c₂ --> c₃ -> Function of a₂,a₁;
coherence by FUNCOP_1:58;

end;

theorem Th25: :: BORSUK_1:25

for b₁ being non empty set
for b₂ being Subset-Family of b₁
for b₃ being Subset of b₂ holds union b₃ is Subset of b₁

proof end;

theorem Th26: :: BORSUK_1:26

for b₁ being set
for b₂ being a_partition of b₁
for b₃, b₄ being Subset of b₂ holds union (b₃ /\ b₄) = (union b₃) /\ (union b₄)

proof end;

theorem Th27: :: BORSUK_1:27

for b₁ being non empty set
for b₂ being a_partition of b₁
for b₃ being Subset of b₂
for b₄ being Subset of b₁ st b₄ = union b₃ holds
b₄ ` = union (b₃ ` )

proof end;

theorem Th28: :: BORSUK_1:28

for b₁ being non empty set
for b₂ being Equivalence_Relation of b₁ holds not Class b₂ is empty ;

registration

let c₁ be non empty set ;
cluster non empty a_partition of a₁;
existence

proof end;

end;

definition

let c₁ be non empty set ;
let c₂ be non empty a_partition of c₁;
func proj c₂ -> Function of a₁,a₂ means :Def1: :: BORSUK_1:def 1
for b₁ being Element of a₁ holds b₁ in a₃ . b₁;
existence

proof end;

correctness

proof end;

end;

:: deftheorem Def1 defines proj BORSUK_1:def 1 :

theorem Th29: :: BORSUK_1:29

for b₁ being non empty set
for b₂ being non empty a_partition of b₁
for b₃ being Element of b₁
for b₄ being Element of b₂ st b₃ in b₄ holds
b₄ = (proj b₂) . b₃

proof end;

theorem Th30: :: BORSUK_1:30

for b₁ being non empty set
for b₂ being non empty a_partition of b₁
for b₃ being Element of b₂ holds b₃ = (proj b₂) " {b₃}

proof end;

theorem Th31: :: BORSUK_1:31

for b₁ being non empty set
for b₂ being non empty a_partition of b₁
for b₃ being Subset of b₂ holds (proj b₂) " b₃ = union b₃

proof end;

theorem Th32: :: BORSUK_1:32

for b₁ being non empty set
for b₂ being non empty a_partition of b₁
for b₃ being Element of b₂ ex b₄ being Element of b₁ st (proj b₂) . b₄ = b₃

proof end;

theorem Th33: :: BORSUK_1:33

for b₁ being non empty set
for b₂ being non empty a_partition of b₁
for b₃ being Subset of b₁ st ( for b₄ being Subset of b₁ st b₄ in b₂ & b₄ meets b₃ holds
b₄ c= b₃ ) holds
b₃ = (proj b₂) " ((proj b₂) .: b₃)

proof end;

theorem Th34: :: BORSUK_1:34

canceled;

theorem Th35: :: BORSUK_1:35

for b₁ being TopStruct
for b₂ being SubSpace of b₁ holds the carrier of b₂ c= the carrier of b₁

proof end;

definition

let c₁, c₂ be non empty TopSpace;
let c₃ be Function of c₁,c₂;
redefine attr a₃ is continuous means :: BORSUK_1:def 2
for b₁ being Point of a₁
for b₂ being a_neighborhood of a₃ . b₁ ex b₃ being a_neighborhood of b₁ st a₃ .: b₃ c= b₂;
compatibility

proof end;

end;

:: deftheorem Def2 defines continuous BORSUK_1:def 2 :

definition

let c₁ be 1-sorted ;
let c₂ be non empty 1-sorted ;
let c₃ be Element of c₂;
func c₁ --> c₃ -> Function of a₁,a₂ equals :: BORSUK_1:def 3
the carrier of a₁ --> a₃;
coherence ;

end;

:: deftheorem Def3 defines --> BORSUK_1:def 3 :

theorem Th36: :: BORSUK_1:36

for b₁, b₂ being non empty TopSpace
for b₃ being Point of b₁ holds b₂ --> b₃ is continuous

proof end;

registration

let c₁, c₂ be non empty TopSpace;
let c₃ be Point of c₂;
cluster a₁ --> a₃ -> continuous ;
coherence by Th36;

end;

registration

let c₁, c₂ be non empty TopSpace;
cluster continuous M6(the carrier of a₁,the carrier of a₂);
existence

proof end;

end;

definition

let c₁, c₂, c₃ be non empty TopSpace;
let c₄ be continuous Function of c₁,c₂;
let c₅ be continuous Function of c₂,c₃;
redefine func * as c₅ * c₄ -> continuous Function of a₁,a₃;
coherence by TOPS_2:58;

end;

theorem Th37: :: BORSUK_1:37

for b₁, b₂ being non empty TopSpace
for b₃ being continuous Function of b₁,b₂
for b₄ being Subset of b₂ holds b₃ " (Int b₄) c= Int (b₃ " b₄)

proof end;

theorem Th38: :: BORSUK_1:38

for b₁, b₂ being non empty TopSpace
for b₃ being Point of b₁
for b₄ being continuous Function of b₂,b₁
for b₅ being a_neighborhood of b₃ holds b₄ " b₅ is a_neighborhood of b₄ " {b₃}

proof end;

definition

let c₁, c₂ be non empty TopSpace;
let c₃ be Point of c₂;
let c₄ be continuous Function of c₁,c₂;
let c₅ be a_neighborhood of c₃;
redefine func " as c₄ " c₅ -> a_neighborhood of a₄ " {a₃};
correctness by Th38;

end;

theorem Th39: :: BORSUK_1:39

for b₁ being non empty TopSpace
for b₂, b₃ being Subset of b₁
for b₄ being a_neighborhood of b₃ st b₂ c= b₃ holds
b₄ is a_neighborhood of b₂

proof end;

theorem Th40: :: BORSUK_1:40

canceled;

theorem Th41: :: BORSUK_1:41

for b₁ being non empty TopSpace
for b₂ being Point of b₁ holds {b₂} is compact

proof end;

theorem Th42: :: BORSUK_1:42

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
( b₃ is compact iff b₄ is compact )

proof end;

definition

let c₁, c₂ be TopSpace;
canceled;
func [:c₁,c₂:] -> strict TopSpace means :Def5: :: BORSUK_1:def 5
( the carrier of a₃ = [:the carrier of a₁,the carrier of a₂:] & the topology of a₃ = { (union b₁) where B is Subset-Family of a₃ : b₁ c= { [:b₂,b₃:] where B is Subset of a₁, B is Subset of a₂ : ( b₂ in the topology of a₁ & b₃ in the topology of a₂ ) } } );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def4 BORSUK_1:def 4 :

:: deftheorem Def5 defines [: BORSUK_1:def 5 :

registration

let c₁, c₂ be non empty TopSpace;
cluster [:a₁,a₂:] -> non empty strict ;
coherence

proof end;

end;

theorem Th43: :: BORSUK_1:43

canceled;

theorem Th44: :: BORSUK_1:44

canceled;

theorem Th45: :: BORSUK_1:45

for b₁, b₂ being TopSpace
for b₃ being Subset of [:b₁,b₂:] holds
( b₃ is open iff ex b₄ being Subset-Family of [:b₁,b₂:] st
( b₃ = union b₄ & ( for b₅ being set st b₅ in b₄ holds
ex b₆ being Subset of b₁ex b₇ being Subset of b₂ st
( b₅ = [:b₆,b₇:] & b₆ is open & b₇ is open ) ) ) )

proof end;

definition

let c₁, c₂ be TopSpace;
let c₃ be Subset of c₁;
let c₄ be Subset of c₂;
redefine func [: as [:c₃,c₄:] -> Subset of [:a₁,a₂:];
correctness

proof end;

end;

definition

let c₁, c₂ be non empty TopSpace;
let c₃ be Point of c₁;
let c₄ be Point of c₂;
redefine func [ as [c₃,c₄] -> Point of [:a₁,a₂:];
correctness

proof end;

end;

theorem Th46: :: BORSUK_1:46

for b₁, b₂ being TopSpace
for b₃ being Subset of b₁
for b₄ being Subset of b₂ st b₃ is open & b₄ is open holds
[:b₃,b₄:] is open

proof end;

theorem Th47: :: BORSUK_1:47

for b₁, b₂ being TopSpace
for b₃ being Subset of b₁
for b₄ being Subset of b₂ holds Int [:b₃,b₄:] = [:(Int b₃),(Int b₄):]

proof end;

theorem Th48: :: BORSUK_1:48

for b₁, b₂ being non empty TopSpace
for b₃ being Point of b₁
for b₄ being Point of b₂
for b₅ being a_neighborhood of b₃
for b₆ being a_neighborhood of b₄ holds [:b₅,b₆:] is a_neighborhood of [b₃,b₄]

proof end;

theorem Th49: :: BORSUK_1:49

for b₁, b₂ being non empty TopSpace
for b₃ being Subset of b₁
for b₄ being Subset of b₂
for b₅ being a_neighborhood of b₃
for b₆ being a_neighborhood of b₄ holds [:b₅,b₆:] is a_neighborhood of [:b₃,b₄:]

proof end;

definition

let c₁, c₂ be non empty TopSpace;
let c₃ be Point of c₁;
let c₄ be Point of c₂;
let c₅ be a_neighborhood of c₃;
let c₆ be a_neighborhood of c₄;
redefine func [: as [:c₅,c₆:] -> a_neighborhood of [a₃,a₄];
correctness by Th48;

end;

theorem Th50: :: BORSUK_1:50

for b₁, b₂ being non empty TopSpace
for b₃ being Point of [:b₁,b₂:] ex b₄ being Point of b₁ex b₅ being Point of b₂ st b₃ = [b₄,b₅]

proof end;

definition

let c₁, c₂ be non empty TopSpace;
let c₃ be Subset of c₁;
let c₄ be Point of c₂;
let c₅ be a_neighborhood of c₃;
let c₆ be a_neighborhood of c₄;
redefine func [: as [:c₅,c₆:] -> a_neighborhood of [:a₃,{a₄}:];
correctness

proof end;

end;

definition

let c₁, c₂ be TopSpace;
let c₃ be Subset of [:c₁,c₂:];
func Base-Appr c₃ -> Subset-Family of [:a₁,a₂:] equals :: BORSUK_1:def 6
{ [:b₁,b₂:] where B is Subset of a₁, B is Subset of a₂ : ( [:b₁,b₂:] c= a₃ & b₁ is open & b₂ is open ) } ;
coherence

proof end;

end;

:: deftheorem Def6 defines Base-Appr BORSUK_1:def 6 :

theorem Th51: :: BORSUK_1:51

for b₁, b₂ being TopSpace
for b₃ being Subset of [:b₁,b₂:] holds Base-Appr b₃ is open

proof end;

theorem Th52: :: BORSUK_1:52

for b₁, b₂ being TopSpace
for b₃, b₄ being Subset of [:b₁,b₂:] st b₃ c= b₄ holds
Base-Appr b₃ c= Base-Appr b₄

proof end;

theorem Th53: :: BORSUK_1:53

for b₁, b₂ being TopSpace
for b₃ being Subset of [:b₁,b₂:] holds union (Base-Appr b₃) c= b₃

proof end;

theorem Th54: :: BORSUK_1:54

for b₁, b₂ being TopSpace
for b₃ being Subset of [:b₁,b₂:] st b₃ is open holds
b₃ = union (Base-Appr b₃)

proof end;

theorem Th55: :: BORSUK_1:55

for b₁, b₂ being TopSpace
for b₃ being Subset of [:b₁,b₂:] holds Int b₃ = union (Base-Appr b₃)

proof end;

definition

let c₁, c₂ be non empty TopSpace;
func Pr1 c₁,c₂ -> Function of bool the carrier of [:a₁,a₂:], bool the carrier of a₁ equals :: BORSUK_1:def 7
.: (pr1 the carrier of a₁,the carrier of a₂);
coherence

proof end;

correctness ;
func Pr2 c₁,c₂ -> Function of bool the carrier of [:a₁,a₂:], bool the carrier of a₂ equals :: BORSUK_1:def 8
.: (pr2 the carrier of a₁,the carrier of a₂);
coherence

proof end;

correctness ;

end;

:: deftheorem Def7 defines Pr1 BORSUK_1:def 7 :

:: deftheorem Def8 defines Pr2 BORSUK_1:def 8 :

theorem Th56: :: BORSUK_1:56

for b₁, b₂ being non empty TopSpace
for b₃ being Subset of [:b₁,b₂:]
for b₄ being Subset-Family of [:b₁,b₂:] st ( for b₅ being set st b₅ in b₄ holds
( b₅ c= b₃ & ex b₆ being Subset of b₁ex b₇ being Subset of b₂ st b₅ = [:b₆,b₇:] ) ) holds
[:(union ((Pr1 b₁,b₂) .: b₄)),(meet ((Pr2 b₁,b₂) .: b₄)):] c= b₃

proof end;

theorem Th57: :: BORSUK_1:57

for b₁, b₂ being non empty TopSpace
for b₃ being Subset-Family of [:b₁,b₂:]
for b₄ being set st b₄ in (Pr1 b₁,b₂) .: b₃ holds
ex b₅ being Subset of [:b₁,b₂:] st
( b₅ in b₃ & b₄ = (pr1 the carrier of b₁,the carrier of b₂) .: b₅ )

proof end;

theorem Th58: :: BORSUK_1:58

for b₁, b₂ being non empty TopSpace
for b₃ being Subset-Family of [:b₁,b₂:]
for b₄ being set st b₄ in (Pr2 b₁,b₂) .: b₃ holds
ex b₅ being Subset of [:b₁,b₂:] st
( b₅ in b₃ & b₄ = (pr2 the carrier of b₁,the carrier of b₂) .: b₅ )

proof end;

theorem Th59: :: BORSUK_1:59

for b₁, b₂ being non empty TopSpace
for b₃ being Subset of [:b₁,b₂:] st b₃ is open holds
for b₄ being Subset of b₁
for b₅ being Subset of b₂ holds
( ( b₄ = (pr1 the carrier of b₁,the carrier of b₂) .: b₃ implies b₄ is open ) & ( b₅ = (pr2 the carrier of b₁,the carrier of b₂) .: b₃ implies b₅ is open ) )

proof end;

definition

let c₁, c₂ be set ;
let c₃ be Function of bool c₁, bool c₂;
let c₄ be Subset-Family of c₁;
redefine func .: as c₃ .: c₄ -> Subset-Family of a₂;
coherence

proof end;

end;

theorem Th60: :: BORSUK_1:60

for b₁, b₂ being non empty TopSpace
for b₃ being Subset-Family of [:b₁,b₂:] st b₃ is open holds
( (Pr1 b₁,b₂) .: b₃ is open & (Pr2 b₁,b₂) .: b₃ is open )

proof end;

theorem Th61: :: BORSUK_1:61

for b₁, b₂ being non empty TopSpace
for b₃ being Subset-Family of [:b₁,b₂:] st ( (Pr1 b₁,b₂) .: b₃ = {} or (Pr2 b₁,b₂) .: b₃ = {} ) holds
b₃ = {}

proof end;

theorem Th62: :: BORSUK_1:62

for b₁, b₂ being non empty TopSpace
for b₃ being Subset-Family of [:b₁,b₂:]
for b₄ being Subset of b₁
for b₅ being Subset of b₂ st b₃ is_a_cover_of [:b₄,b₅:] holds
( ( b₅ <> {} implies (Pr1 b₁,b₂) .: b₃ is_a_cover_of b₄ ) & ( b₄ <> {} implies (Pr2 b₁,b₂) .: b₃ is_a_cover_of b₅ ) )

proof end;

theorem Th63: :: BORSUK_1:63

for b₁, b₂ being TopSpace
for b₃ being Subset-Family of b₁
for b₄ being Subset of b₁ st b₃ is_a_cover_of b₄ holds
ex b₅ being Subset-Family of b₁ st
( b₅ c= b₃ & b₅ is_a_cover_of b₄ & ( for b₆ being set st b₆ in b₅ holds
b₆ meets b₄ ) )

proof end;

theorem Th64: :: BORSUK_1:64

for b₁, b₂ being non empty TopSpace
for b₃ being Subset-Family of b₁
for b₄ being Subset-Family of [:b₁,b₂:] st b₃ is finite & b₃ c= (Pr1 b₁,b₂) .: b₄ holds
ex b₅ being Subset-Family of [:b₁,b₂:] st
( b₅ c= b₄ & b₅ is finite & b₃ = (Pr1 b₁,b₂) .: b₅ )

proof end;

theorem Th65: :: BORSUK_1:65

for b₁, b₂ being non empty TopSpace
for b₃ being Subset of b₁
for b₄ being Subset of b₂ st [:b₃,b₄:] <> {} holds
( (Pr1 b₁,b₂) . [:b₃,b₄:] = b₃ & (Pr2 b₁,b₂) . [:b₃,b₄:] = b₄ ) by Th13;

theorem Th66: :: BORSUK_1:66

for b₁, b₂ being non empty TopSpace holds
( (Pr1 b₁,b₂) . {} = {} & (Pr2 b₁,b₂) . {} = {} ) by FUNCT_3:9;

theorem Th67: :: BORSUK_1:67

for b₁, b₂ being non empty TopSpace
for b₃ being Point of b₁
for b₄ being Subset of b₂ st b₄ is compact holds
for b₅ being a_neighborhood of [:b₄,{b₃}:] ex b₆ being a_neighborhood of b₄ex b₇ being a_neighborhood of b₃ st [:b₆,b₇:] c= b₅

proof end;

definition

let c₁ be 1-sorted ;
func TrivDecomp c₁ -> a_partition of the carrier of a₁ equals :: BORSUK_1:def 9
Class (id the carrier of a₁);
coherence ;

end;

:: deftheorem Def9 defines TrivDecomp BORSUK_1:def 9 :

registration

let c₁ be non empty 1-sorted ;
cluster TrivDecomp a₁ -> non empty ;
coherence ;

end;

theorem Th68: :: BORSUK_1:68

for b₁ being non empty TopSpace
for b₂ being Subset of b₁ st b₂ in TrivDecomp b₁ holds
ex b₃ being Point of b₁ st b₂ = {b₃}

proof end;

Lemma56: for b₁ being non empty TopSpace
for b₂ being Subset of b₁ st b₂ in TrivDecomp b₁ holds
for b₃ being a_neighborhood of b₂ ex b₄ being Subset of b₁ st
( b₄ is open & b₂ c= b₄ & b₄ c= b₃ & ( for b₅ being Subset of b₁ st b₅ in TrivDecomp b₁ & b₅ meets b₄ holds
b₅ c= b₄ ) )

proof end;

definition

let c₁ be TopSpace;
let c₂ be a_partition of the carrier of c₁;
func space c₂ -> strict TopSpace means :Def10: :: BORSUK_1:def 10
( the carrier of a₃ = a₂ & the topology of a₃ = { b₁ where B is Subset of a₂ : union b₁ in the topology of a₁ } );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def10 defines space BORSUK_1:def 10 :

registration

let c₁ be non empty TopSpace;
let c₂ be non empty a_partition of the carrier of c₁;
cluster space a₂ -> non empty strict ;
coherence

proof end;

end;

theorem Th69: :: BORSUK_1:69

for b₁ being non empty TopSpace
for b₂ being non empty a_partition of the carrier of b₁
for b₃ being Subset of b₂ holds
( union b₃ in the topology of b₁ iff b₃ in the topology of (space b₂) )

proof end;

definition

let c₁ be non empty TopSpace;
let c₂ be non empty a_partition of the carrier of c₁;
func Proj c₂ -> continuous Function of a₁,(space a₂) equals :: BORSUK_1:def 11
proj a₂;
coherence

proof end;

correctness ;

end;

:: deftheorem Def11 defines Proj BORSUK_1:def 11 :

theorem Th70: :: BORSUK_1:70

for b₁ being non empty TopSpace
for b₂ being non empty a_partition of the carrier of b₁
for b₃ being Point of b₁ holds b₃ in (Proj b₂) . b₃ by Def1;

theorem Th71: :: BORSUK_1:71

for b₁ being non empty TopSpace
for b₂ being non empty a_partition of the carrier of b₁
for b₃ being Point of (space b₂) ex b₄ being Point of b₁ st (Proj b₂) . b₄ = b₃

proof end;

theorem Th72: :: BORSUK_1:72

for b₁ being non empty TopSpace
for b₂ being non empty a_partition of the carrier of b₁ holds rng (Proj b₂) = the carrier of (space b₂)

proof end;

definition

let c₁ be non empty TopSpace;
let c₂ be non empty SubSpace of c₁;
let c₃ be non empty a_partition of the carrier of c₂;
func TrivExt c₃ -> non empty a_partition of the carrier of a₁ equals :: BORSUK_1:def 12
a₃ \/ { {b₁} where B is Point of a₁ : not b₁ in the carrier of a₂ } ;
coherence

proof end;

correctness ;

end;

:: deftheorem Def12 defines TrivExt BORSUK_1:def 12 :

theorem Th73: :: BORSUK_1:73

for b₁ being non empty TopSpace
for b₂ being non empty SubSpace of b₁
for b₃ being non empty a_partition of the carrier of b₂ holds b₃ c= TrivExt b₃ by XBOOLE_1:7;

theorem Th74: :: BORSUK_1:74

for b₁ being non empty TopSpace
for b₂ being non empty SubSpace of b₁
for b₃ being non empty a_partition of the carrier of b₂
for b₄ being Subset of b₁ holds
( not b₄ in TrivExt b₃ or b₄ in b₃ or ex b₅ being Point of b₁ st
( not b₅ in [#] b₂ & b₄ = {b₅} ) )

proof end;

theorem Th75: :: BORSUK_1:75

for b₁ being non empty TopSpace
for b₂ being non empty SubSpace of b₁
for b₃ being non empty a_partition of the carrier of b₂
for b₄ being Point of b₁ st not b₄ in the carrier of b₂ holds
{b₄} in TrivExt b₃

proof end;

theorem Th76: :: BORSUK_1:76

for b₁ being non empty TopSpace
for b₂ being non empty SubSpace of b₁
for b₃ being non empty a_partition of the carrier of b₂
for b₄ being Point of b₁ st b₄ in the carrier of b₂ holds
(Proj (TrivExt b₃)) . b₄ = (Proj b₃) . b₄

proof end;

theorem Th77: :: BORSUK_1:77

for b₁ being non empty TopSpace
for b₂ being non empty SubSpace of b₁
for b₃ being non empty a_partition of the carrier of b₂
for b₄ being Point of b₁ st not b₄ in the carrier of b₂ holds
(Proj (TrivExt b₃)) . b₄ = {b₄}

proof end;

theorem Th78: :: BORSUK_1:78

for b₁ being non empty TopSpace
for b₂ being non empty SubSpace of b₁
for b₃ being non empty a_partition of the carrier of b₂
for b₄, b₅ being Point of b₁ st not b₄ in the carrier of b₂ & (Proj (TrivExt b₃)) . b₄ = (Proj (TrivExt b₃)) . b₅ holds
b₄ = b₅

proof end;

theorem Th79: :: BORSUK_1:79

for b₁ being non empty TopSpace
for b₂ being non empty SubSpace of b₁
for b₃ being non empty a_partition of the carrier of b₂
for b₄ being Point of b₁ st (Proj (TrivExt b₃)) . b₄ in the carrier of (space b₃) holds
b₄ in the carrier of b₂

proof end;

theorem Th80: :: BORSUK_1:80

for b₁ being non empty TopSpace
for b₂ being non empty SubSpace of b₁
for b₃ being non empty a_partition of the carrier of b₂
for b₄ being set st b₄ in the carrier of b₂ holds
(Proj (TrivExt b₃)) . b₄ in the carrier of (space b₃)

proof end;

definition

let c₁ be non empty TopSpace;
mode u.s.c._decomposition of c₁ -> non empty a_partition of the carrier of a₁ means :Def13: :: BORSUK_1:def 13
for b₁ being Subset of a₁ st b₁ in a₂ holds
for b₂ being a_neighborhood of b₁ ex b₃ being Subset of a₁ st
( b₃ is open & b₁ c= b₃ & b₃ c= b₂ & ( for b₄ being Subset of a₁ st b₄ in a₂ & b₄ meets b₃ holds
b₄ c= b₃ ) );
correctness

proof end;

end;

:: deftheorem Def13 defines u.s.c._decomposition BORSUK_1:def 13 :

theorem Th81: :: BORSUK_1:81

for b₁ being non empty TopSpace
for b₂ being u.s.c._decomposition of b₁
for b₃ being Point of (space b₂)
for b₄ being a_neighborhood of (Proj b₂) " {b₃} holds (Proj b₂) .: b₄ is a_neighborhood of b₃

proof end;

theorem Th82: :: BORSUK_1:82

for b₁ being non empty TopSpace holds TrivDecomp b₁ is u.s.c._decomposition of b₁

proof end;

definition

let c₁ be TopSpace;
let c₂ be SubSpace of c₁;
attr a₂ is closed means :Def14: :: BORSUK_1:def 14
for b₁ being Subset of a₁ st b₁ = the carrier of a₂ holds
b₁ is closed;

end;

:: deftheorem Def14 defines closed BORSUK_1:def 14 :

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

proof end;

registration

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

proof end;

end;

registration

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

proof end;

end;

definition

let c₁ be non empty TopSpace;
let c₂ be non empty closed SubSpace of c₁;
let c₃ be u.s.c._decomposition of c₂;
redefine func TrivExt as TrivExt c₃ -> u.s.c._decomposition of a₁;
correctness

proof end;

end;

definition

let c₁ be non empty TopSpace;
let c₂ be u.s.c._decomposition of c₁;
attr a₂ is DECOMPOSITION-like means :Def15: :: BORSUK_1:def 15
for b₁ being Subset of a₁ st b₁ in a₂ holds
b₁ is compact;

end;

:: deftheorem Def15 defines DECOMPOSITION-like BORSUK_1:def 15 :

registration

let c₁ be non empty TopSpace;
cluster non empty DECOMPOSITION-like u.s.c._decomposition of a₁;
existence

proof end;

end;

definition

let c₁ be non empty TopSpace;
mode DECOMPOSITION of a₁ is DECOMPOSITION-like u.s.c._decomposition of a₁;

end;

definition

let c₁ be non empty TopSpace;
let c₂ be non empty closed SubSpace of c₁;
let c₃ be DECOMPOSITION of c₂;
redefine func TrivExt as TrivExt c₃ -> DECOMPOSITION of a₁;
correctness

proof end;

end;

definition

let c₁ be non empty TopSpace;
let c₂ be non empty closed SubSpace of c₁;
let c₃ be DECOMPOSITION of c₂;
redefine func space as space c₃ -> strict closed SubSpace of space (TrivExt a₃);
correctness

proof end;

end;

Lemma74: TopSpaceMetr RealSpace = TopStruct(# the carrier of RealSpace ,(Family_open_set RealSpace ) #)
by PCOMPS_1:def 6;

definition

func I[01] -> TopStruct means :Def16: :: BORSUK_1:def 16
for b₁ being Subset of (TopSpaceMetr RealSpace ) st b₁ = [.0,1.] holds
a₁ = (TopSpaceMetr RealSpace ) | b₁;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def16 defines I[01] BORSUK_1:def 16 :

registration

cluster I[01] -> non empty strict TopSpace-like ;
coherence

proof end;

end;

theorem Th83: :: BORSUK_1:83

the carrier of I[01] = [.0,1.]

proof end;

definition

func 0[01] -> Point of I[01] equals :: BORSUK_1:def 17
0;
coherence by Th83, RCOMP_1:15;
func 1[01] -> Point of I[01] equals :: BORSUK_1:def 18
1;
coherence by Th83, RCOMP_1:15;

end;

:: deftheorem Def17 defines 0[01] BORSUK_1:def 17 :

:: deftheorem Def18 defines 1[01] BORSUK_1:def 18 :

definition

let c₁ be non empty TopSpace;
let c₂ be non empty SubSpace of c₁;
let c₃ be Function of c₁,c₂;
attr a₃ is being_a_retraction means :Def19: :: BORSUK_1:def 19
for b₁ being Point of a₁ st b₁ in the carrier of a₂ holds
a₃ . b₁ = b₁;

end;

:: deftheorem Def19 defines being_a_retraction BORSUK_1:def 19 :

notation

let c₁ be non empty TopSpace;
let c₂ be non empty SubSpace of c₁;
let c₃ be Function of c₁,c₂;
synonym c₃ is_a_retraction for being_a_retraction c₃;

end;

definition

let c₁ be non empty TopSpace;
let c₂ be non empty SubSpace of c₁;
pred c₂ is_a_retract_of c₁ means :: BORSUK_1:def 20
ex b₁ being continuous Function of a₁,a₂ st b₁ is_a_retraction ;
pred c₂ is_an_SDR_of c₁ means :: BORSUK_1:def 21
ex b₁ being continuous Function of [:a₁,I[01] :],a₁ st
for b₂ being Point of a₁ holds
( b₁ . [b₂,0[01] ] = b₂ & b₁ . [b₂,1[01] ] in the carrier of a₂ & ( b₂ in the carrier of a₂ implies for b₃ being Point of I[01] holds b₁ . [b₂,b₃] = b₂ ) );

end;

:: deftheorem Def20 defines is_a_retract_of BORSUK_1:def 20 :

:: deftheorem Def21 defines is_an_SDR_of BORSUK_1:def 21 :

theorem Th84: :: BORSUK_1:84

for b₁ being non empty TopSpace
for b₂ being non empty closed SubSpace of b₁
for b₃ being DECOMPOSITION of b₂ st b₂ is_a_retract_of b₁ holds
space b₃ is_a_retract_of space (TrivExt b₃)

proof end;

theorem Th85: :: BORSUK_1:85

for b₁ being non empty TopSpace
for b₂ being non empty closed SubSpace of b₁
for b₃ being DECOMPOSITION of b₂ st b₂ is_an_SDR_of b₁ holds
space b₃ is_an_SDR_of space (TrivExt b₃)

proof end;