:: BORSUK_1 semantic presentation

theorem :: BORSUK_1:1

canceled;

theorem :: BORSUK_1:2

canceled;

theorem :: BORSUK_1:3

canceled;

theorem Th4: :: BORSUK_1:4

for X being set
for A being Subset of X holds (id X) " A = A

proof end;

theorem Th5: :: BORSUK_1:5

for X, X1 being set
for F being Function st X c= F " X1 holds
F .: X c= X1

proof end;

theorem Th6: :: BORSUK_1:6

for X, u, X1 being set holds (X --> u) .: X1 c= {u}

proof end;

theorem :: BORSUK_1:7

canceled;

theorem :: BORSUK_1:8

canceled;

theorem Th9: :: BORSUK_1:9

for e, X, Y being set st e c= [:X,Y:] holds
(.: (pr1 X,Y)) . e = (pr1 X,Y) .: e

proof end;

theorem Th10: :: BORSUK_1:10

for e, X, Y being set st e c= [:X,Y:] holds
(.: (pr2 X,Y)) . e = (pr2 X,Y) .: e

proof end;

theorem :: BORSUK_1:11

canceled;

theorem Th12: :: BORSUK_1:12

for X, Y being set
for X1 being Subset of X
for Y1 being Subset of Y st [:X1,Y1:] <> {} holds
( (pr1 X,Y) .: [:X1,Y1:] = X1 & (pr2 X,Y) .: [:X1,Y1:] = Y1 )

proof end;

theorem Th13: :: BORSUK_1:13

for X, Y being set
for X1 being Subset of X
for Y1 being Subset of Y st [:X1,Y1:] <> {} holds
( (.: (pr1 X,Y)) . [:X1,Y1:] = X1 & (.: (pr2 X,Y)) . [:X1,Y1:] = Y1 )

proof end;

theorem Th14: :: BORSUK_1:14

for X, Y being set
for A being Subset of [:X,Y:]
for H being Subset-Family of [:X,Y:] st ( for e being set st e in H holds
( e c= A & ex X1 being Subset of X ex Y1 being Subset of Y st e = [:X1,Y1:] ) ) holds
[:(union ((.: (pr1 X,Y)) .: H)),(meet ((.: (pr2 X,Y)) .: H)):] c= A

proof end;

theorem :: BORSUK_1:15

for X, Y being set
for A being Subset of [:X,Y:]
for H being Subset-Family of [:X,Y:] st ( for e being set st e in H holds
( e c= A & ex X1 being Subset of X ex Y1 being Subset of Y st e = [:X1,Y1:] ) ) holds
[:(meet ((.: (pr1 X,Y)) .: H)),(union ((.: (pr2 X,Y)) .: H)):] c= A

proof end;

theorem Th16: :: BORSUK_1:16

for X being set
for Y being non empty set
for f being Function of X,Y
for H being Subset-Family of X holds union ((.: f) .: H) = f .: (union H)

proof end;

theorem Th17: :: BORSUK_1:17

for X being set
for a being Subset-Family of X holds union (union a) = union { (union A) where A is Subset of X : A in a }

proof end;

theorem Th18: :: BORSUK_1:18

for X being set
for D being Subset-Family of X st union D = X holds
for A being Subset of D
for B being Subset of X st B = union A holds
B ` c= union (A ` )

proof end;

theorem Th19: :: BORSUK_1:19

for X, Y, Z being non empty set
for F being Function of X,Y
for G being Function of X,Z st ( for x, x' being Element of X st F . x = F . x' holds
G . x = G . x' ) holds
ex H being Function of Y,Z st H * F = G

proof end;

theorem Th20: :: BORSUK_1:20

for X, Y, Z being non empty set
for y being Element of Y
for F being Function of X,Y
for G being Function of Y,Z holds F " {y} c= (G * F) " {(G . y)}

proof end;

theorem Th21: :: BORSUK_1:21

for X, Y, Z being non empty set
for F being Function of X,Y
for x being Element of X
for z being Element of Z holds [:F,(id Z):] . [x,z] = [(F . x),z]

proof end;

theorem :: BORSUK_1:22

canceled;

theorem Th23: :: BORSUK_1:23

for X, Y, Z being non empty set
for F being Function of X,Y
for A being Subset of X
for B being Subset of Z holds [:F,(id Z):] .: [:A,B:] = [:(F .: A),B:]

proof end;

theorem Th24: :: BORSUK_1:24

for X, Y, Z being non empty set
for F being Function of X,Y
for y being Element of Y
for z being Element of Z holds [:F,(id Z):] " {[y,z]} = [:(F " {y}),{z}:]

proof end;

definition

let B be non empty set ;
let A be set ;
let x be Element of B;
:: original: -->
redefine func A --> x -> Function of A,B;
coherence by FUNCOP_1:58;

end;

theorem Th25: :: BORSUK_1:25

for X being non empty set
for D being Subset-Family of X
for A being Subset of D holds union A is Subset of X

proof end;

theorem Th26: :: BORSUK_1:26

for X being set
for D being a_partition of X
for A, B being Subset of D holds union (A /\ B) = (union A) /\ (union B)

proof end;

theorem Th27: :: BORSUK_1:27

for X being non empty set
for D being a_partition of X
for A being Subset of D
for B being Subset of X st B = union A holds
B ` = union (A ` )

proof end;

theorem :: BORSUK_1:28

for X being non empty set
for E being Equivalence_Relation of X holds not Class E is empty ;

registration

let X be non empty set ;
cluster non empty a_partition of X;
existence

proof end;

end;

definition

let X be non empty set ;
let D be non empty a_partition of X;
func proj D -> Function of X,D means :Def1: :: BORSUK_1:def 1
for p being Element of X holds p in it . p;
existence

proof end;

correctness

proof end;

end;

:: deftheorem Def1 defines proj BORSUK_1:def 1 :

theorem Th29: :: BORSUK_1:29

for X being non empty set
for D being non empty a_partition of X
for p being Element of X
for A being Element of D st p in A holds
A = (proj D) . p

proof end;

theorem Th30: :: BORSUK_1:30

for X being non empty set
for D being non empty a_partition of X
for p being Element of D holds p = (proj D) " {p}

proof end;

theorem Th31: :: BORSUK_1:31

for X being non empty set
for D being non empty a_partition of X
for A being Subset of D holds (proj D) " A = union A

proof end;

theorem Th32: :: BORSUK_1:32

for X being non empty set
for D being non empty a_partition of X
for W being Element of D ex W' being Element of X st (proj D) . W' = W

proof end;

theorem Th33: :: BORSUK_1:33

for X being non empty set
for D being non empty a_partition of X
for W being Subset of X st ( for B being Subset of X st B in D & B meets W holds
B c= W ) holds
W = (proj D) " ((proj D) .: W)

proof end;

theorem :: BORSUK_1:34

canceled;

theorem Th35: :: BORSUK_1:35

for X being TopStruct
for Y being SubSpace of X holds the carrier of Y c= the carrier of X

proof end;

definition

let X, Y be non empty TopSpace;
let F be Function of X,Y;
redefine attr F is continuous means :: BORSUK_1:def 2
for W being Point of X
for G being a_neighborhood of F . W ex H being a_neighborhood of W st F .: H c= G;
compatibility

proof end;

end;

:: deftheorem defines continuous BORSUK_1:def 2 :

definition

let X be 1-sorted ;
let Y be non empty 1-sorted ;
let y be Element of Y;
func X --> y -> Function of X,Y equals :: BORSUK_1:def 3
the carrier of X --> y;
coherence ;

end;

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

theorem Th36: :: BORSUK_1:36

for Y, X being non empty TopSpace
for y being Point of Y holds X --> y is continuous

proof end;

registration

let X, Y be non empty TopSpace;
let y be Point of Y;
cluster X --> y -> continuous ;
coherence by Th36;

end;

registration

let S, T be non empty TopSpace;
cluster continuous M6(the carrier of S,the carrier of T);
existence

proof end;

end;

definition

let X, Y, Z be non empty TopSpace;
let F be continuous Function of X,Y;
let G be continuous Function of Y,Z;
:: original: *
redefine func G * F -> continuous Function of X,Z;
coherence by TOPS_2:58;

end;

theorem Th37: :: BORSUK_1:37

for X, Y being non empty TopSpace
for A being continuous Function of X,Y
for G being Subset of Y holds A " (Int G) c= Int (A " G)

proof end;

theorem Th38: :: BORSUK_1:38

for Y, X being non empty TopSpace
for W being Point of Y
for A being continuous Function of X,Y
for G being a_neighborhood of W holds A " G is a_neighborhood of A " {W}

proof end;

definition

let X, Y be non empty TopSpace;
let W be Point of Y;
let A be continuous Function of X,Y;
let G be a_neighborhood of W;
:: original: "
redefine func A " G -> a_neighborhood of A " {W};
correctness by Th38;

end;

theorem Th39: :: BORSUK_1:39

for X being non empty TopSpace
for A, B being Subset of X
for U being a_neighborhood of B st A c= B holds
U is a_neighborhood of A

proof end;

theorem :: BORSUK_1:40

canceled;

theorem Th41: :: BORSUK_1:41

for X being non empty TopSpace
for x being Point of X holds {x} is compact

proof end;

theorem Th42: :: BORSUK_1:42

for X being TopStruct
for Y being SubSpace of X
for A being Subset of X
for B being Subset of Y st A = B holds
( A is compact iff B is compact )

proof end;

definition

let X, Y be TopSpace;
canceled;
func [:X,Y:] -> strict TopSpace means :Def5: :: BORSUK_1:def 5
( the carrier of it = [:the carrier of X,the carrier of Y:] & the topology of it = { (union A) where A is Subset-Family of it : A c= { [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y ) } } );
existence

proof end;

uniqueness ;

end;

:: deftheorem BORSUK_1:def 4 :

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

registration

let X, Y be non empty TopSpace;
cluster [:X,Y:] -> non empty strict ;
coherence

proof end;

end;

theorem :: BORSUK_1:43

canceled;

theorem :: BORSUK_1:44

canceled;

theorem Th45: :: BORSUK_1:45

for X, Y being TopSpace
for B being Subset of [:X,Y:] holds
( B is open iff ex A being Subset-Family of [:X,Y:] st
( B = union A & ( for e being set st e in A holds
ex X1 being Subset of X ex Y1 being Subset of Y st
( e = [:X1,Y1:] & X1 is open & Y1 is open ) ) ) )

proof end;

definition

let X, Y be TopSpace;
let A be Subset of X;
let B be Subset of Y;
:: original: [:
redefine func [:A,B:] -> Subset of [:X,Y:];
correctness

proof end;

end;

definition

let X, Y be non empty TopSpace;
let x be Point of X;
let y be Point of Y;
:: original: [
redefine func [x,y] -> Point of [:X,Y:];
correctness

proof end;

end;

theorem Th46: :: BORSUK_1:46

for X, Y being TopSpace
for V being Subset of X
for W being Subset of Y st V is open & W is open holds
[:V,W:] is open

proof end;

theorem Th47: :: BORSUK_1:47

for X, Y being TopSpace
for V being Subset of X
for W being Subset of Y holds Int [:V,W:] = [:(Int V),(Int W):]

proof end;

theorem Th48: :: BORSUK_1:48

for X, Y being non empty TopSpace
for x being Point of X
for y being Point of Y
for V being a_neighborhood of x
for W being a_neighborhood of y holds [:V,W:] is a_neighborhood of [x,y]

proof end;

theorem Th49: :: BORSUK_1:49

for X, Y being non empty TopSpace
for A being Subset of X
for B being Subset of Y
for V being a_neighborhood of A
for W being a_neighborhood of B holds [:V,W:] is a_neighborhood of [:A,B:]

proof end;

definition

let X, Y be non empty TopSpace;
let x be Point of X;
let y be Point of Y;
let V be a_neighborhood of x;
let W be a_neighborhood of y;
:: original: [:
redefine func [:V,W:] -> a_neighborhood of [x,y];
correctness by Th48;

end;

theorem Th50: :: BORSUK_1:50

for X, Y being non empty TopSpace
for XT being Point of [:X,Y:] ex W being Point of X ex T being Point of Y st XT = [W,T]

proof end;

definition

let X, Y be non empty TopSpace;
let A be Subset of X;
let t be Point of Y;
let V be a_neighborhood of A;
let W be a_neighborhood of t;
:: original: [:
redefine func [:V,W:] -> a_neighborhood of [:A,{t}:];
correctness

proof end;

end;

definition

let X, Y be TopSpace;
let A be Subset of [:X,Y:];
func Base-Appr A -> Subset-Family of [:X,Y:] equals :: BORSUK_1:def 6
{ [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( [:X1,Y1:] c= A & X1 is open & Y1 is open ) } ;
coherence

proof end;

end;

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

theorem Th51: :: BORSUK_1:51

for X, Y being TopSpace
for A being Subset of [:X,Y:] holds Base-Appr A is open

proof end;

theorem Th52: :: BORSUK_1:52

for X, Y being TopSpace
for A, B being Subset of [:X,Y:] st A c= B holds
Base-Appr A c= Base-Appr B

proof end;

theorem Th53: :: BORSUK_1:53

for X, Y being TopSpace
for A being Subset of [:X,Y:] holds union (Base-Appr A) c= A

proof end;

theorem Th54: :: BORSUK_1:54

for X, Y being TopSpace
for A being Subset of [:X,Y:] st A is open holds
A = union (Base-Appr A)

proof end;

theorem Th55: :: BORSUK_1:55

for X, Y being TopSpace
for A being Subset of [:X,Y:] holds Int A = union (Base-Appr A)

proof end;

definition

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

proof end;

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

proof end;

correctness ;

end;

:: deftheorem defines Pr1 BORSUK_1:def 7 :

:: deftheorem defines Pr2 BORSUK_1:def 8 :

theorem Th56: :: BORSUK_1:56

for X, Y being non empty TopSpace
for A being Subset of [:X,Y:]
for H being Subset-Family of [:X,Y:] st ( for e being set st e in H holds
( e c= A & ex X1 being Subset of X ex Y1 being Subset of Y st e = [:X1,Y1:] ) ) holds
[:(union ((Pr1 X,Y) .: H)),(meet ((Pr2 X,Y) .: H)):] c= A

proof end;

theorem Th57: :: BORSUK_1:57

for X, Y being non empty TopSpace
for H being Subset-Family of [:X,Y:]
for C being set st C in (Pr1 X,Y) .: H holds
ex D being Subset of [:X,Y:] st
( D in H & C = (pr1 the carrier of X,the carrier of Y) .: D )

proof end;

theorem Th58: :: BORSUK_1:58

for X, Y being non empty TopSpace
for H being Subset-Family of [:X,Y:]
for C being set st C in (Pr2 X,Y) .: H holds
ex D being Subset of [:X,Y:] st
( D in H & C = (pr2 the carrier of X,the carrier of Y) .: D )

proof end;

theorem Th59: :: BORSUK_1:59

for X, Y being non empty TopSpace
for D being Subset of [:X,Y:] st D is open holds
for X1 being Subset of X
for Y1 being Subset of Y holds
( ( X1 = (pr1 the carrier of X,the carrier of Y) .: D implies X1 is open ) & ( Y1 = (pr2 the carrier of X,the carrier of Y) .: D implies Y1 is open ) )

proof end;

definition

let X, Y be set ;
let f be Function of bool X, bool Y;
let R be Subset-Family of X;
:: original: .:
redefine func f .: R -> Subset-Family of Y;
coherence

proof end;

end;

theorem Th60: :: BORSUK_1:60

for X, Y being non empty TopSpace
for H being Subset-Family of [:X,Y:] st H is open holds
( (Pr1 X,Y) .: H is open & (Pr2 X,Y) .: H is open )

proof end;

theorem Th61: :: BORSUK_1:61

for X, Y being non empty TopSpace
for H being Subset-Family of [:X,Y:] st ( (Pr1 X,Y) .: H = {} or (Pr2 X,Y) .: H = {} ) holds
H = {}

proof end;

theorem Th62: :: BORSUK_1:62

for X, Y being non empty TopSpace
for H being Subset-Family of [:X,Y:]
for X1 being Subset of X
for Y1 being Subset of Y st H is_a_cover_of [:X1,Y1:] holds
( ( Y1 <> {} implies (Pr1 X,Y) .: H is_a_cover_of X1 ) & ( X1 <> {} implies (Pr2 X,Y) .: H is_a_cover_of Y1 ) )

proof end;

theorem Th63: :: BORSUK_1:63

for X, Y being TopSpace
for H being Subset-Family of X
for Y being Subset of X st H is_a_cover_of Y holds
ex F being Subset-Family of X st
( F c= H & F is_a_cover_of Y & ( for C being set st C in F holds
C meets Y ) )

proof end;

theorem Th64: :: BORSUK_1:64

for X, Y being non empty TopSpace
for F being Subset-Family of X
for H being Subset-Family of [:X,Y:] st F is finite & F c= (Pr1 X,Y) .: H holds
ex G being Subset-Family of [:X,Y:] st
( G c= H & G is finite & F = (Pr1 X,Y) .: G )

proof end;

theorem :: BORSUK_1:65

for X, Y being non empty TopSpace
for X1 being Subset of X
for Y1 being Subset of Y st [:X1,Y1:] <> {} holds
( (Pr1 X,Y) . [:X1,Y1:] = X1 & (Pr2 X,Y) . [:X1,Y1:] = Y1 ) by Th13;

theorem :: BORSUK_1:66

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

theorem Th67: :: BORSUK_1:67

for Y, X being non empty TopSpace
for t being Point of Y
for A being Subset of X st A is compact holds
for G being a_neighborhood of [:A,{t}:] ex V being a_neighborhood of A ex W being a_neighborhood of t st [:V,W:] c= G

proof end;

definition

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

end;

:: deftheorem defines TrivDecomp BORSUK_1:def 9 :

registration

let X be non empty 1-sorted ;
cluster TrivDecomp X -> non empty ;
coherence ;

end;

theorem Th68: :: BORSUK_1:68

for X being non empty TopSpace
for A being Subset of X st A in TrivDecomp X holds
ex x being Point of X st A = {x}

proof end;

Lm1: for X being non empty TopSpace
for A being Subset of X st A in TrivDecomp X holds
for V being a_neighborhood of A ex W being Subset of X st
( W is open & A c= W & W c= V & ( for B being Subset of X st B in TrivDecomp X & B meets W holds
B c= W ) )

proof end;

definition

let X be TopSpace;
let D be a_partition of the carrier of X;
func space D -> strict TopSpace means :Def10: :: BORSUK_1:def 10
( the carrier of it = D & the topology of it = { A where A is Subset of D : union A in the topology of X } );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def10 defines space BORSUK_1:def 10 :

registration

let X be non empty TopSpace;
let D be non empty a_partition of the carrier of X;
cluster space D -> non empty strict ;
coherence

proof end;

end;

theorem Th69: :: BORSUK_1:69

for X being non empty TopSpace
for D being non empty a_partition of the carrier of X
for A being Subset of D holds
( union A in the topology of X iff A in the topology of (space D) )

proof end;

definition

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

proof end;

correctness ;

end;

:: deftheorem defines Proj BORSUK_1:def 11 :

theorem :: BORSUK_1:70

for X being non empty TopSpace
for D being non empty a_partition of the carrier of X
for W being Point of X holds W in (Proj D) . W by Def1;

theorem Th71: :: BORSUK_1:71

for X being non empty TopSpace
for D being non empty a_partition of the carrier of X
for W being Point of (space D) ex W' being Point of X st (Proj D) . W' = W

proof end;

theorem Th72: :: BORSUK_1:72

for X being non empty TopSpace
for D being non empty a_partition of the carrier of X holds rng (Proj D) = the carrier of (space D)

proof end;

definition

let XX be non empty TopSpace;
let X be non empty SubSpace of XX;
let D be non empty a_partition of the carrier of X;
func TrivExt D -> non empty a_partition of the carrier of XX equals :: BORSUK_1:def 12
D \/ { {p} where p is Point of XX : not p in the carrier of X } ;
coherence

proof end;

correctness ;

end;

:: deftheorem defines TrivExt BORSUK_1:def 12 :

theorem :: BORSUK_1:73

for XX being non empty TopSpace
for X being non empty SubSpace of XX
for D being non empty a_partition of the carrier of X holds D c= TrivExt D by XBOOLE_1:7;

theorem Th74: :: BORSUK_1:74

for XX being non empty TopSpace
for X being non empty SubSpace of XX
for D being non empty a_partition of the carrier of X
for A being Subset of XX holds
( not A in TrivExt D or A in D or ex x being Point of XX st
( not x in [#] X & A = {x} ) )

proof end;

theorem Th75: :: BORSUK_1:75

for XX being non empty TopSpace
for X being non empty SubSpace of XX
for D being non empty a_partition of the carrier of X
for x being Point of XX st not x in the carrier of X holds
{x} in TrivExt D

proof end;

theorem Th76: :: BORSUK_1:76

for XX being non empty TopSpace
for X being non empty SubSpace of XX
for D being non empty a_partition of the carrier of X
for W being Point of XX st W in the carrier of X holds
(Proj (TrivExt D)) . W = (Proj D) . W

proof end;

theorem Th77: :: BORSUK_1:77

for XX being non empty TopSpace
for X being non empty SubSpace of XX
for D being non empty a_partition of the carrier of X
for W being Point of XX st not W in the carrier of X holds
(Proj (TrivExt D)) . W = {W}

proof end;

theorem Th78: :: BORSUK_1:78

for XX being non empty TopSpace
for X being non empty SubSpace of XX
for D being non empty a_partition of the carrier of X
for W, W' being Point of XX st not W in the carrier of X & (Proj (TrivExt D)) . W = (Proj (TrivExt D)) . W' holds
W = W'

proof end;

theorem Th79: :: BORSUK_1:79

for XX being non empty TopSpace
for X being non empty SubSpace of XX
for D being non empty a_partition of the carrier of X
for e being Point of XX st (Proj (TrivExt D)) . e in the carrier of (space D) holds
e in the carrier of X

proof end;

theorem Th80: :: BORSUK_1:80

for XX being non empty TopSpace
for X being non empty SubSpace of XX
for D being non empty a_partition of the carrier of X
for e being set st e in the carrier of X holds
(Proj (TrivExt D)) . e in the carrier of (space D)

proof end;

definition

let X be non empty TopSpace;
mode u.s.c._decomposition of X -> non empty a_partition of the carrier of X means :Def13: :: BORSUK_1:def 13
for A being Subset of X st A in it holds
for V being a_neighborhood of A ex W being Subset of X st
( W is open & A c= W & W c= V & ( for B being Subset of X st B in it & B meets W holds
B c= W ) );
correctness

proof end;

end;

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

theorem Th81: :: BORSUK_1:81

for X being non empty TopSpace
for D being u.s.c._decomposition of X
for t being Point of (space D)
for G being a_neighborhood of (Proj D) " {t} holds (Proj D) .: G is a_neighborhood of t

proof end;

theorem Th82: :: BORSUK_1:82

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

proof end;

definition

let X be TopSpace;
let IT be SubSpace of X;
attr IT is closed means :Def14: :: BORSUK_1:def 14
for A being Subset of X st A = the carrier of IT holds
A is closed;

end;

:: deftheorem Def14 defines closed BORSUK_1:def 14 :

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

proof end;

registration

let X be TopSpace;
cluster strict closed SubSpace of X;
existence

proof end;

end;

registration

let X be non empty TopSpace;
cluster non empty strict closed SubSpace of X;
existence

proof end;

end;

definition

let XX be non empty TopSpace;
let X be non empty closed SubSpace of XX;
let D be u.s.c._decomposition of X;
:: original: TrivExt
redefine func TrivExt D -> u.s.c._decomposition of XX;
correctness

proof end;

end;

definition

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

end;

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

registration

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

proof end;

end;

definition

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

end;

definition

let XX be non empty TopSpace;
let X be non empty closed SubSpace of XX;
let D be DECOMPOSITION of X;
:: original: TrivExt
redefine func TrivExt D -> DECOMPOSITION of XX;
correctness

proof end;

end;

definition

let X be non empty TopSpace;
let Y be non empty closed SubSpace of X;
let D be DECOMPOSITION of Y;
:: original: space
redefine func space D -> strict closed SubSpace of space (TrivExt D);
correctness

proof end;

end;

Lm3: 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 P being Subset of (TopSpaceMetr RealSpace ) st P = [.0,1.] holds
it = (TopSpaceMetr RealSpace ) | P;
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 defines 0[01] BORSUK_1:def 17 :

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

definition

let A be non empty TopSpace;
let B be non empty SubSpace of A;
let F be Function of A,B;
attr F is being_a_retraction means :Def19: :: BORSUK_1:def 19
for W being Point of A st W in the carrier of B holds
F . W = W;

end;

:: deftheorem Def19 defines being_a_retraction BORSUK_1:def 19 :

notation

let A be non empty TopSpace;
let B be non empty SubSpace of A;
let F be Function of A,B;
synonym F is_a_retraction for being_a_retraction F;

end;

definition

let X be non empty TopSpace;
let Y be non empty SubSpace of X;
pred Y is_a_retract_of X means :: BORSUK_1:def 20
ex F being continuous Function of X,Y st F is_a_retraction ;
pred Y is_an_SDR_of X means :: BORSUK_1:def 21
ex H being continuous Function of [:X,I[01] :],X st
for A being Point of X holds
( H . [A,0[01] ] = A & H . [A,1[01] ] in the carrier of Y & ( A in the carrier of Y implies for T being Point of I[01] holds H . [A,T] = A ) );

end;

:: deftheorem defines is_a_retract_of BORSUK_1:def 20 :

:: deftheorem defines is_an_SDR_of BORSUK_1:def 21 :

theorem :: BORSUK_1:84

for XX being non empty TopSpace
for X being non empty closed SubSpace of XX
for D being DECOMPOSITION of X st X is_a_retract_of XX holds
space D is_a_retract_of space (TrivExt D)

proof end;

theorem :: BORSUK_1:85

for XX being non empty TopSpace
for X being non empty closed SubSpace of XX
for D being DECOMPOSITION of X st X is_an_SDR_of XX holds
space D is_an_SDR_of space (TrivExt D)

proof end;