:: by Andrzej Trybulec

::

:: Received August 1, 1991

:: Copyright (c) 1991 Association of Mizar Users

begin

theorem :: BORSUK_1:1

canceled;

theorem :: BORSUK_1:2

canceled;

theorem :: BORSUK_1:3

canceled;

theorem :: BORSUK_1:4

canceled;

theorem :: BORSUK_1:5

canceled;

theorem :: BORSUK_1:6

canceled;

theorem :: BORSUK_1:7

canceled;

theorem :: BORSUK_1:8

canceled;

theorem :: BORSUK_1:9

canceled;

theorem :: BORSUK_1:10

canceled;

theorem :: BORSUK_1:11

canceled;

theorem :: BORSUK_1:12

canceled;

theorem :: BORSUK_1:13

canceled;

theorem :: BORSUK_1:14

canceled;

theorem :: BORSUK_1:15

canceled;

theorem :: BORSUK_1:16

canceled;

theorem :: BORSUK_1:17

canceled;

theorem :: BORSUK_1:18

canceled;

theorem :: BORSUK_1:19

canceled;

theorem :: BORSUK_1:20

canceled;

theorem :: BORSUK_1:21

canceled;

theorem :: BORSUK_1:22

canceled;

theorem :: BORSUK_1:23

canceled;

theorem :: BORSUK_1:24

canceled;

theorem :: BORSUK_1:25

canceled;

theorem :: BORSUK_1:26

canceled;

theorem :: BORSUK_1:27

canceled;

theorem :: BORSUK_1:28

canceled;

theorem :: BORSUK_1:29

canceled;

theorem :: BORSUK_1:30

canceled;

theorem :: BORSUK_1:31

canceled;

theorem :: BORSUK_1:32

canceled;

theorem :: BORSUK_1:33

canceled;

theorem :: BORSUK_1:34

canceled;

theorem Th35: :: BORSUK_1:35

proof end;

definition

canceled;

canceled;

let X, Y be non empty TopSpace;

let F be Function of X,Y;

redefine attr F is continuous means :: BORSUK_1:def 3

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

( F is continuous iff 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 )

end;
canceled;

let X, Y be non empty TopSpace;

let F be Function of X,Y;

redefine attr F is continuous means :: BORSUK_1:def 3

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

( F is continuous iff 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 )

proof end;

:: deftheorem BORSUK_1:def 1 :

canceled;

:: deftheorem BORSUK_1:def 2 :

canceled;

:: deftheorem defines continuous BORSUK_1:def 3 :

for X, Y being non empty TopSpace

for F being Function of X,Y holds

( F is continuous iff 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 );

registration

let X, Y, Z be non empty TopSpace;

let F be continuous Function of X,Y;

let G be continuous Function of Y,Z;

cluster F * G -> continuous Function of X,Z;

coherence

for b_{1} being Function of X,Z st b_{1} = G * F holds

b_{1} is continuous
by TOPS_2:58;

end;
let F be continuous Function of X,Y;

let G be continuous Function of Y,Z;

cluster F * G -> continuous Function of X,Z;

coherence

for b

b

theorem :: BORSUK_1:36

canceled;

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)

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}

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

coherence

A " G is a_neighborhood of A " {W};

by Th38;

end;
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

coherence

A " G is a_neighborhood of A " {W};

by Th38;

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

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;

registration

let X be non empty TopSpace;

let x be Point of X;

cluster {x} -> compact Subset of X;

coherence

for b_{1} being Subset of X st b_{1} = {x} holds

b_{1} is compact

end;
let x be Point of X;

cluster {x} -> compact Subset of X;

coherence

for b

b

proof end;

theorem :: BORSUK_1:41

canceled;

begin

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

ex b_{1} being strict TopSpace st

( the carrier of b_{1} = [: the carrier of X, the carrier of Y:] & the topology of b_{1} = { (union A) where A is Subset-Family of b_{1} : 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 ) } } )

for b_{1}, b_{2} being strict TopSpace st the carrier of b_{1} = [: the carrier of X, the carrier of Y:] & the topology of b_{1} = { (union A) where A is Subset-Family of b_{1} : 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 ) } } & the carrier of b_{2} = [: the carrier of X, the carrier of Y:] & the topology of b_{2} = { (union A) where A is Subset-Family of b_{2} : 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 ) } } holds

b_{1} = b_{2}
;

end;
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

ex b

( the carrier of b

proof end;

uniqueness for b

b

:: deftheorem BORSUK_1:def 4 :

canceled;

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

for X, Y being TopSpace

for b

( b

registration

let X, Y be non empty TopSpace;

cluster [:X,Y:] -> non empty strict ;

coherence

not [:X,Y:] is empty

end;
cluster [:X,Y:] -> non empty strict ;

coherence

not [:X,Y:] is empty

proof end;

theorem :: BORSUK_1:42

canceled;

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 ) ) ) )

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

coherence

[:A,B:] is Subset of [:X,Y:];

end;
let A be Subset of X;

let B be Subset of Y;

:: original: [:

redefine func [:A,B:] -> Subset of [:X,Y:];

correctness

coherence

[:A,B:] is Subset of [:X,Y:];

proof 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

coherence

[x,y] is Point of [:X,Y:];

end;
let x be Point of X;

let y be Point of Y;

:: original: [

redefine func [x,y] -> Point of [:X,Y:];

correctness

coherence

[x,y] is Point of [:X,Y:];

proof 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

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):]

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]

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:]

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

coherence

[:V,W:] is a_neighborhood of [x,y];

by Th48;

end;
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

coherence

[:V,W:] is a_neighborhood of [x,y];

by Th48;

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]

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

coherence

[:V,W:] is a_neighborhood of [:A,{t}:];

end;
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

coherence

[:V,W:] is a_neighborhood of [:A,{t}:];

proof 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

{ [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( [:X1,Y1:] c= A & X1 is open & Y1 is open ) } is Subset-Family of [:X,Y:]

end;
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

{ [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( [:X1,Y1:] c= A & X1 is open & Y1 is open ) } is Subset-Family of [:X,Y:]

proof end;

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

for X, Y being TopSpace

for A being Subset of [:X,Y:] holds Base-Appr A = { [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( [:X1,Y1:] c= A & X1 is open & Y1 is open ) } ;

theorem :: BORSUK_1:51

canceled;

registration

let X, Y be TopSpace;

let A be Subset of [:X,Y:];

cluster Base-Appr A -> open ;

coherence

Base-Appr A is open

end;
let A be Subset of [:X,Y:];

cluster Base-Appr A -> open ;

coherence

Base-Appr A is open

proof end;

theorem Th52: :: BORSUK_1:52

proof end;

theorem Th53: :: BORSUK_1:53

proof end;

theorem Th54: :: BORSUK_1:54

proof end;

theorem Th55: :: BORSUK_1:55

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

.: (pr1 ( the carrier of X, the carrier of Y)) is Function of (bool the carrier of [:X,Y:]),(bool the carrier of X)

;

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

.: (pr2 ( the carrier of X, the carrier of Y)) is Function of (bool the carrier of [:X,Y:]),(bool the carrier of Y)

;

end;
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

.: (pr1 ( the carrier of X, the carrier of Y)) is Function of (bool the carrier of [:X,Y:]),(bool the carrier of X)

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

.: (pr2 ( the carrier of X, the carrier of Y)) is Function of (bool the carrier of [:X,Y:]),(bool the carrier of Y)

proof end;

correctness ;

:: deftheorem defines Pr1 BORSUK_1:def 7 :

for X, Y being non empty TopSpace holds Pr1 (X,Y) = .: (pr1 ( the carrier of X, the carrier of Y));

:: deftheorem defines Pr2 BORSUK_1:def 8 :

for X, Y being non empty TopSpace holds Pr2 (X,Y) = .: (pr2 ( the carrier of X, the carrier of Y));

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

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 )

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 )

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 ) )

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;

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 )

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 = {}

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 Cover of [:X1,Y1:] holds

( ( Y1 <> {} implies (Pr1 (X,Y)) .: H is Cover of X1 ) & ( X1 <> {} implies (Pr2 (X,Y)) .: H is Cover of Y1 ) )

for H being Subset-Family of [:X,Y:]

for X1 being Subset of X

for Y1 being Subset of Y st H is Cover of [:X1,Y1:] holds

( ( Y1 <> {} implies (Pr1 (X,Y)) .: H is Cover of X1 ) & ( X1 <> {} implies (Pr2 (X,Y)) .: H is 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 Cover of Y holds

ex F being Subset-Family of X st

( F c= H & F is Cover of Y & ( for C being set st C in F holds

C meets Y ) )

for H being Subset-Family of X

for Y being Subset of X st H is Cover of Y holds

ex F being Subset-Family of X st

( F c= H & F is 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 )

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 EQREL_1:59;

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 EQREL_1:59;

theorem :: BORSUK_1:66

canceled;

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

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;

begin

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

Class (id the carrier of X) is a_partition of the carrier of X ;

end;
func TrivDecomp X -> a_partition of the carrier of X equals :: BORSUK_1:def 9

Class (id the carrier of X);

coherence

Class (id the carrier of X) is a_partition of the carrier of X ;

:: deftheorem defines TrivDecomp BORSUK_1:def 9 :

for X being 1-sorted holds TrivDecomp X = Class (id the carrier of X);

registration

let X be non empty 1-sorted ;

cluster TrivDecomp X -> non empty ;

coherence

not TrivDecomp X is empty ;

end;
cluster TrivDecomp X -> non empty ;

coherence

not TrivDecomp X is empty ;

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}

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

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

ex b_{1} being strict TopSpace st

( the carrier of b_{1} = D & the topology of b_{1} = { A where A is Subset of D : union A in the topology of X } )

for b_{1}, b_{2} being strict TopSpace st the carrier of b_{1} = D & the topology of b_{1} = { A where A is Subset of D : union A in the topology of X } & the carrier of b_{2} = D & the topology of b_{2} = { A where A is Subset of D : union A in the topology of X } holds

b_{1} = b_{2}
;

end;
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

ex b

( the carrier of b

proof end;

uniqueness for b

b

:: deftheorem Def10 defines space BORSUK_1:def 10 :

for X being TopSpace

for D being a_partition of the carrier of X

for b

( b

registration

let X be non empty TopSpace;

let D be a_partition of the carrier of X;

cluster space D -> non empty strict ;

coherence

not space D is empty by Def10;

end;
let D be a_partition of the carrier of X;

cluster space D -> non empty strict ;

coherence

not space D is empty by Def10;

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) )

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

proj D is continuous Function of X,(space D)

;

end;
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

proj D is continuous Function of X,(space D)

proof end;

correctness ;

:: deftheorem defines Proj BORSUK_1:def 11 :

for X being non empty TopSpace

for D being non empty a_partition of the carrier of X holds Proj D = proj D;

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 EQREL_1:def 12;

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 EQREL_1:def 12;

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 W9 being Point of X st (Proj D) . W9 = W

for D being non empty a_partition of the carrier of X

for W being Point of (space D) ex W9 being Point of X st (Proj D) . W9 = 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)

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

D \/ { {p} where p is Point of XX : not p in the carrier of X } is non empty a_partition of the carrier of XX

;

end;
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

D \/ { {p} where p is Point of XX : not p in the carrier of X } is non empty a_partition of the carrier of XX

proof end;

correctness ;

:: deftheorem defines TrivExt BORSUK_1:def 12 :

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 TrivExt D = D \/ { {p} where p is Point of XX : not p in the carrier of X } ;

theorem :: BORSUK_1:73

canceled;

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} ) )

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

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

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}

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, W9 being Point of XX st not W in the carrier of X & (Proj (TrivExt D)) . W = (Proj (TrivExt D)) . W9 holds

W = W9

for X being non empty SubSpace of XX

for D being non empty a_partition of the carrier of X

for W, W9 being Point of XX st not W in the carrier of X & (Proj (TrivExt D)) . W = (Proj (TrivExt D)) . W9 holds

W = W9

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

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)

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;

begin

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

existence

ex b_{1} being non empty a_partition of the carrier of X st

for A being Subset of X st A in b_{1} 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 b_{1} & B meets W holds

B c= W ) );

end;
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

existence

ex b

for A being Subset of X st A in b

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 b

B c= W ) );

proof end;

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

for X being non empty TopSpace

for b

( b

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 b

B c= W ) ) );

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

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

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;
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 ;

:: deftheorem Def14 defines closed BORSUK_1:def 14 :

for X being TopSpace

for IT being SubSpace of X holds

( IT is closed iff for A being Subset of X st A = the carrier of IT holds

A is closed );

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 TopSpace-like closed SubSpace of X;

existence

ex b_{1} being SubSpace of X st

( b_{1} is strict & b_{1} is closed )

end;
cluster strict TopSpace-like closed SubSpace of X;

existence

ex b

( b

proof end;

registration

let X be non empty TopSpace;

cluster non empty strict TopSpace-like closed SubSpace of X;

existence

ex b_{1} being SubSpace of X st

( b_{1} is strict & b_{1} is closed & not b_{1} is empty )

end;
cluster non empty strict TopSpace-like closed SubSpace of X;

existence

ex b

( b

proof 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

coherence

TrivExt D is u.s.c._decomposition of XX;

end;
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

coherence

TrivExt D is u.s.c._decomposition of XX;

proof 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;
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 ;

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

for X being non empty TopSpace

for IT being u.s.c._decomposition of X holds

( IT is DECOMPOSITION-like iff for A being Subset of X st A in IT holds

A is compact );

registration

let X be non empty TopSpace;

cluster non empty with_non-empty_elements DECOMPOSITION-like u.s.c._decomposition of X;

existence

ex b_{1} being u.s.c._decomposition of X st b_{1} is DECOMPOSITION-like

end;
cluster non empty with_non-empty_elements DECOMPOSITION-like u.s.c._decomposition of X;

existence

ex b

proof end;

definition

let X be non empty TopSpace;

mode DECOMPOSITION of X is DECOMPOSITION-like u.s.c._decomposition of X;

end;
mode DECOMPOSITION of X is DECOMPOSITION-like u.s.c._decomposition of X;

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

coherence

TrivExt D is DECOMPOSITION of XX;

end;
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

coherence

TrivExt D is DECOMPOSITION of XX;

proof 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

coherence

space D is strict closed SubSpace of space (TrivExt D);

end;
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

coherence

space D is strict closed SubSpace of space (TrivExt D);

proof end;

begin

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

ex b_{1} being TopStruct st

for P being Subset of (TopSpaceMetr RealSpace) st P = [.0,1.] holds

b_{1} = (TopSpaceMetr RealSpace) | P

for b_{1}, b_{2} being TopStruct st ( for P being Subset of (TopSpaceMetr RealSpace) st P = [.0,1.] holds

b_{1} = (TopSpaceMetr RealSpace) | P ) & ( for P being Subset of (TopSpaceMetr RealSpace) st P = [.0,1.] holds

b_{2} = (TopSpaceMetr RealSpace) | P ) holds

b_{1} = b_{2}

end;
for P being Subset of (TopSpaceMetr RealSpace) st P = [.0,1.] holds

it = (TopSpaceMetr RealSpace) | P;

existence

ex b

for P being Subset of (TopSpaceMetr RealSpace) st P = [.0,1.] holds

b

proof end;

uniqueness for b

b

b

b

proof end;

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

for b

( b

b

registration

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

coherence

( I[01] is strict & not I[01] is empty & I[01] is TopSpace-like )

end;
coherence

( I[01] is strict & not I[01] is empty & I[01] is TopSpace-like )

proof end;

theorem Th83: :: BORSUK_1:83

proof end;

definition

func 0[01] -> Point of I[01] equals :: BORSUK_1:def 17

0 ;

coherence

0 is Point of I[01] by Th83, XXREAL_1:1;

func 1[01] -> Point of I[01] equals :: BORSUK_1:def 18

1;

coherence

1 is Point of I[01] by Th83, XXREAL_1:1;

end;
0 ;

coherence

0 is Point of I[01] by Th83, XXREAL_1:1;

func 1[01] -> Point of I[01] equals :: BORSUK_1:def 18

1;

coherence

1 is Point of I[01] by Th83, XXREAL_1:1;

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

0[01] = 0 ;

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

1[01] = 1;

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;
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;

:: deftheorem Def19 defines being_a_retraction BORSUK_1:def 19 :

for A being non empty TopSpace

for B being non empty SubSpace of A

for F being Function of A,B holds

( F is being_a_retraction iff for W being Point of A st W in the carrier of B holds

F . W = W );

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 being_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;
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 being_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 ) );

:: deftheorem defines is_a_retract_of BORSUK_1:def 20 :

for X being non empty TopSpace

for Y being non empty SubSpace of X holds

( Y is_a_retract_of X iff ex F being continuous Function of X,Y st F is being_a_retraction );

:: deftheorem defines is_an_SDR_of BORSUK_1:def 21 :

for X being non empty TopSpace

for Y being non empty SubSpace of X holds

( Y is_an_SDR_of X iff 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 ) ) );

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)

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)

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;

theorem :: BORSUK_1:86

proof end;