:: by Adam Grabowski and Artur Korni{\l}owicz

::

:: Received March 18, 2004

:: Copyright (c) 2004-2019 Association of Mizar Users

scheme :: BORSUK_6:sch 1

ExFunc3CondD{ F_{1}() -> non empty set , P_{1}[ set ], P_{2}[ set ], P_{3}[ set ], F_{2}( set ) -> set , F_{3}( set ) -> set , F_{4}( set ) -> set } :

ExFunc3CondD{ F

ex f being Function st

( dom f = F_{1}() & ( for c being Element of F_{1}() holds

( ( P_{1}[c] implies f . c = F_{2}(c) ) & ( P_{2}[c] implies f . c = F_{3}(c) ) & ( P_{3}[c] implies f . c = F_{4}(c) ) ) ) )

provided( dom f = F

( ( P

A1:
for c being Element of F_{1}() holds

( ( P_{1}[c] implies not P_{2}[c] ) & ( P_{1}[c] implies not P_{3}[c] ) & ( P_{2}[c] implies not P_{3}[c] ) )
and

A2: for c being Element of F_{1}() holds

( P_{1}[c] or P_{2}[c] or P_{3}[c] )

( ( P

A2: for c being Element of F

( P

proof end;

theorem Th2: :: BORSUK_6:2

for a, b, x being Real st a <= x & x <= b holds

(x - a) / (b - a) in the carrier of (Closed-Interval-TSpace (0,1))

(x - a) / (b - a) in the carrier of (Closed-Interval-TSpace (0,1))

proof end;

theorem Th9: :: BORSUK_6:9

for a, b, c, d being Point of I[01] st a <= b & c <= d holds

[:[.a,b.],[.c,d.]:] is non empty compact Subset of [:I[01],I[01]:]

[:[.a,b.],[.c,d.]:] is non empty compact Subset of [:I[01],I[01]:]

proof end;

theorem Th10: :: BORSUK_6:10

for S, T being Subset of (TOP-REAL 2) st S = { p where p is Point of (TOP-REAL 2) : p `2 <= (2 * (p `1)) - 1 } & T = { p where p is Point of (TOP-REAL 2) : p `2 <= p `1 } holds

(AffineMap (1,0,(1 / 2),(1 / 2))) .: S = T

(AffineMap (1,0,(1 / 2),(1 / 2))) .: S = T

proof end;

theorem Th11: :: BORSUK_6:11

for S, T being Subset of (TOP-REAL 2) st S = { p where p is Point of (TOP-REAL 2) : p `2 >= (2 * (p `1)) - 1 } & T = { p where p is Point of (TOP-REAL 2) : p `2 >= p `1 } holds

(AffineMap (1,0,(1 / 2),(1 / 2))) .: S = T

(AffineMap (1,0,(1 / 2),(1 / 2))) .: S = T

proof end;

theorem Th12: :: BORSUK_6:12

for S, T being Subset of (TOP-REAL 2) st S = { p where p is Point of (TOP-REAL 2) : p `2 >= 1 - (2 * (p `1)) } & T = { p where p is Point of (TOP-REAL 2) : p `2 >= - (p `1) } holds

(AffineMap (1,0,(1 / 2),(- (1 / 2)))) .: S = T

(AffineMap (1,0,(1 / 2),(- (1 / 2)))) .: S = T

proof end;

theorem Th13: :: BORSUK_6:13

for S, T being Subset of (TOP-REAL 2) st S = { p where p is Point of (TOP-REAL 2) : p `2 <= 1 - (2 * (p `1)) } & T = { p where p is Point of (TOP-REAL 2) : p `2 <= - (p `1) } holds

(AffineMap (1,0,(1 / 2),(- (1 / 2)))) .: S = T

(AffineMap (1,0,(1 / 2),(- (1 / 2)))) .: S = T

proof end;

theorem :: BORSUK_6:14

for T being non empty 1-sorted holds

( T is real-membered iff for x being Element of T holds x is real )

( T is real-membered iff for x being Element of T holds x is real )

proof end;

registration

existence

ex b_{1} being 1-sorted st

( not b_{1} is empty & b_{1} is real-membered )

ex b_{1} being TopSpace st

( not b_{1} is empty & b_{1} is real-membered )

end;
ex b

( not b

proof end;

existence ex b

( not b

proof end;

registration
end;

registration

let T be real-membered TopStruct ;

coherence

for b_{1} being SubSpace of T holds b_{1} is real-membered
;

end;
coherence

for b

registration

let S, T be non empty real-membered TopSpace;

let p be Element of [:S,T:];

coherence

p `1 is real

p `2 is real

end;
let p be Element of [:S,T:];

coherence

p `1 is real

proof end;

coherence p `2 is real

proof end;

registration

let T be non empty SubSpace of [:I[01],I[01]:];

let x be Point of T;

coherence

x `1 is real

x `2 is real

end;
let x be Point of T;

coherence

x `1 is real

proof end;

coherence x `2 is real

proof end;

theorem Th19: :: BORSUK_6:19

{ p where p is Point of (TOP-REAL 2) : ( p `2 >= 1 - (2 * (p `1)) & p `2 >= (2 * (p `1)) - 1 ) } is closed Subset of (TOP-REAL 2)

proof end;

theorem Th23: :: BORSUK_6:23

{ p where p is Point of [:R^1,R^1:] : ( p `2 >= 1 - (2 * (p `1)) & p `2 >= (2 * (p `1)) - 1 ) } is closed Subset of [:R^1,R^1:]

proof end;

theorem Th24: :: BORSUK_6:24

{ p where p is Point of [:I[01],I[01]:] : p `2 <= 1 - (2 * (p `1)) } is non empty closed Subset of [:I[01],I[01]:]

proof end;

theorem Th25: :: BORSUK_6:25

{ p where p is Point of [:I[01],I[01]:] : ( p `2 >= 1 - (2 * (p `1)) & p `2 >= (2 * (p `1)) - 1 ) } is non empty closed Subset of [:I[01],I[01]:]

proof end;

theorem Th26: :: BORSUK_6:26

{ p where p is Point of [:I[01],I[01]:] : p `2 <= (2 * (p `1)) - 1 } is non empty closed Subset of [:I[01],I[01]:]

proof end;

theorem Th27: :: BORSUK_6:27

for S, T being non empty TopSpace

for p being Point of [:S,T:] holds

( p `1 is Point of S & p `2 is Point of T )

for p being Point of [:S,T:] holds

( p `1 is Point of S & p `2 is Point of T )

proof end;

theorem Th28: :: BORSUK_6:28

for A, B being Subset of [:I[01],I[01]:] st A = [:[.0,(1 / 2).],[.0,1.]:] & B = [:[.(1 / 2),1.],[.0,1.]:] holds

([#] ([:I[01],I[01]:] | A)) \/ ([#] ([:I[01],I[01]:] | B)) = [#] [:I[01],I[01]:]

([#] ([:I[01],I[01]:] | A)) \/ ([#] ([:I[01],I[01]:] | B)) = [#] [:I[01],I[01]:]

proof end;

theorem Th29: :: BORSUK_6:29

for A, B being Subset of [:I[01],I[01]:] st A = [:[.0,(1 / 2).],[.0,1.]:] & B = [:[.(1 / 2),1.],[.0,1.]:] holds

([#] ([:I[01],I[01]:] | A)) /\ ([#] ([:I[01],I[01]:] | B)) = [:{(1 / 2)},[.0,1.]:]

([#] ([:I[01],I[01]:] | A)) /\ ([#] ([:I[01],I[01]:] | B)) = [:{(1 / 2)},[.0,1.]:]

proof end;

registration

let T be TopStruct ;

existence

ex b_{1} being Subset of T st

( b_{1} is empty & b_{1} is compact )

end;
existence

ex b

( b

proof end;

definition

let a, b, c, d be Real;

coherence

(L[01] (((#) (c,d)),((c,d) (#)))) * (P[01] (a,b,((#) (0,1)),((0,1) (#)))) is Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (c,d));

;

end;
func L[01] (a,b,c,d) -> Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (c,d)) equals :: BORSUK_6:def 1

(L[01] (((#) (c,d)),((c,d) (#)))) * (P[01] (a,b,((#) (0,1)),((0,1) (#))));

correctness (L[01] (((#) (c,d)),((c,d) (#)))) * (P[01] (a,b,((#) (0,1)),((0,1) (#))));

coherence

(L[01] (((#) (c,d)),((c,d) (#)))) * (P[01] (a,b,((#) (0,1)),((0,1) (#)))) is Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (c,d));

;

:: deftheorem defines L[01] BORSUK_6:def 1 :

for a, b, c, d being Real holds L[01] (a,b,c,d) = (L[01] (((#) (c,d)),((c,d) (#)))) * (P[01] (a,b,((#) (0,1)),((0,1) (#))));

for a, b, c, d being Real holds L[01] (a,b,c,d) = (L[01] (((#) (c,d)),((c,d) (#)))) * (P[01] (a,b,((#) (0,1)),((0,1) (#))));

theorem Th33: :: BORSUK_6:33

for a, b, c, d being Real st a < b & c < d holds

( (L[01] (a,b,c,d)) . a = c & (L[01] (a,b,c,d)) . b = d )

( (L[01] (a,b,c,d)) . a = c & (L[01] (a,b,c,d)) . b = d )

proof end;

theorem Th34: :: BORSUK_6:34

for a, b, c, d being Real st a < b & c <= d holds

L[01] (a,b,c,d) is continuous Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (c,d))

L[01] (a,b,c,d) is continuous Function of (Closed-Interval-TSpace (a,b)),(Closed-Interval-TSpace (c,d))

proof end;

theorem Th35: :: BORSUK_6:35

for a, b, c, d being Real st a < b & c <= d holds

for x being Real st a <= x & x <= b holds

(L[01] (a,b,c,d)) . x = (((d - c) / (b - a)) * (x - a)) + c

for x being Real st a <= x & x <= b holds

(L[01] (a,b,c,d)) . x = (((d - c) / (b - a)) * (x - a)) + c

proof end;

theorem Th36: :: BORSUK_6:36

for f1, f2 being Function of [:I[01],I[01]:],I[01] st f1 is continuous & f2 is continuous & ( for p being Point of [:I[01],I[01]:] holds (f1 . p) * (f2 . p) is Point of I[01] ) holds

ex g being Function of [:I[01],I[01]:],I[01] st

( ( for p being Point of [:I[01],I[01]:]

for r1, r2 being Real st f1 . p = r1 & f2 . p = r2 holds

g . p = r1 * r2 ) & g is continuous )

ex g being Function of [:I[01],I[01]:],I[01] st

( ( for p being Point of [:I[01],I[01]:]

for r1, r2 being Real st f1 . p = r1 & f2 . p = r2 holds

g . p = r1 * r2 ) & g is continuous )

proof end;

theorem Th37: :: BORSUK_6:37

for f1, f2 being Function of [:I[01],I[01]:],I[01] st f1 is continuous & f2 is continuous & ( for p being Point of [:I[01],I[01]:] holds (f1 . p) + (f2 . p) is Point of I[01] ) holds

ex g being Function of [:I[01],I[01]:],I[01] st

( ( for p being Point of [:I[01],I[01]:]

for r1, r2 being Real st f1 . p = r1 & f2 . p = r2 holds

g . p = r1 + r2 ) & g is continuous )

ex g being Function of [:I[01],I[01]:],I[01] st

( ( for p being Point of [:I[01],I[01]:]

for r1, r2 being Real st f1 . p = r1 & f2 . p = r2 holds

g . p = r1 + r2 ) & g is continuous )

proof end;

theorem :: BORSUK_6:38

for f1, f2 being Function of [:I[01],I[01]:],I[01] st f1 is continuous & f2 is continuous & ( for p being Point of [:I[01],I[01]:] holds (f1 . p) - (f2 . p) is Point of I[01] ) holds

ex g being Function of [:I[01],I[01]:],I[01] st

( ( for p being Point of [:I[01],I[01]:]

for r1, r2 being Real st f1 . p = r1 & f2 . p = r2 holds

g . p = r1 - r2 ) & g is continuous )

ex g being Function of [:I[01],I[01]:],I[01] st

( ( for p being Point of [:I[01],I[01]:]

for r1, r2 being Real st f1 . p = r1 & f2 . p = r2 holds

g . p = r1 - r2 ) & g is continuous )

proof end;

theorem Th39: :: BORSUK_6:39

for T being non empty TopSpace

for a, b being Point of T

for P being Path of a,b st P is continuous holds

P * (L[01] (((0,1) (#)),((#) (0,1)))) is continuous Function of I[01],T

for a, b being Point of T

for P being Path of a,b st P is continuous holds

P * (L[01] (((0,1) (#)),((#) (0,1)))) is continuous Function of I[01],T

proof end;

theorem Th40: :: BORSUK_6:40

for X being non empty TopStruct

for a, b being Point of X

for P being Path of a,b st P . 0 = a & P . 1 = b holds

( (P * (L[01] (((0,1) (#)),((#) (0,1))))) . 0 = b & (P * (L[01] (((0,1) (#)),((#) (0,1))))) . 1 = a )

for a, b being Point of X

for P being Path of a,b st P . 0 = a & P . 1 = b holds

( (P * (L[01] (((0,1) (#)),((#) (0,1))))) . 0 = b & (P * (L[01] (((0,1) (#)),((#) (0,1))))) . 1 = a )

proof end;

theorem Th41: :: BORSUK_6:41

for T being non empty TopSpace

for a, b being Point of T

for P being Path of a,b st P is continuous & P . 0 = a & P . 1 = b holds

( - P is continuous & (- P) . 0 = b & (- P) . 1 = a )

for a, b being Point of T

for P being Path of a,b st P is continuous & P . 0 = a & P . 1 = b holds

( - P is continuous & (- P) . 0 = b & (- P) . 1 = a )

proof end;

definition

let T be non empty TopSpace;

let a, b be Point of T;

:: original: are_connected

redefine pred a,b are_connected ;

reflexivity

for a being Point of T holds R62(T,b_{1},b_{1})

for a, b being Point of T st R62(T,b_{1},b_{2}) holds

R62(T,b_{2},b_{1})

end;
let a, b be Point of T;

:: original: are_connected

redefine pred a,b are_connected ;

reflexivity

for a being Point of T holds R62(T,b

proof end;

symmetry for a, b being Point of T st R62(T,b

R62(T,b

proof end;

theorem Th42: :: BORSUK_6:42

for T being non empty TopSpace

for a, b, c being Point of T st a,b are_connected & b,c are_connected holds

a,c are_connected

for a, b, c being Point of T st a,b are_connected & b,c are_connected holds

a,c are_connected

proof end;

theorem Th43: :: BORSUK_6:43

for T being non empty TopSpace

for a, b being Point of T st a,b are_connected holds

for A being Path of a,b holds A = - (- A)

for a, b being Point of T st a,b are_connected holds

for A being Path of a,b holds A = - (- A)

proof end;

theorem :: BORSUK_6:44

for T being non empty pathwise_connected TopSpace

for a, b being Point of T

for A being Path of a,b holds A = - (- A) by Th43, BORSUK_2:def 3;

for a, b being Point of T

for A being Path of a,b holds A = - (- A) by Th43, BORSUK_2:def 3;

definition

let T be non empty pathwise_connected TopSpace;

let a, b, c be Point of T;

let P be Path of a,b;

let Q be Path of b,c;

for b_{1} being Path of a,c holds

( b_{1} = P + Q iff for t being Point of I[01] holds

( ( t <= 1 / 2 implies b_{1} . t = P . (2 * t) ) & ( 1 / 2 <= t implies b_{1} . t = Q . ((2 * t) - 1) ) ) )

end;
let a, b, c be Point of T;

let P be Path of a,b;

let Q be Path of b,c;

redefine func P + Q means :: BORSUK_6:def 2

for t being Point of I[01] holds

( ( t <= 1 / 2 implies it . t = P . (2 * t) ) & ( 1 / 2 <= t implies it . t = Q . ((2 * t) - 1) ) );

compatibility for t being Point of I[01] holds

( ( t <= 1 / 2 implies it . t = P . (2 * t) ) & ( 1 / 2 <= t implies it . t = Q . ((2 * t) - 1) ) );

for b

( b

( ( t <= 1 / 2 implies b

proof end;

:: deftheorem defines + BORSUK_6:def 2 :

for T being non empty pathwise_connected TopSpace

for a, b, c being Point of T

for P being Path of a,b

for Q being Path of b,c

for b_{7} being Path of a,c holds

( b_{7} = P + Q iff for t being Point of I[01] holds

( ( t <= 1 / 2 implies b_{7} . t = P . (2 * t) ) & ( 1 / 2 <= t implies b_{7} . t = Q . ((2 * t) - 1) ) ) );

for T being non empty pathwise_connected TopSpace

for a, b, c being Point of T

for P being Path of a,b

for Q being Path of b,c

for b

( b

( ( t <= 1 / 2 implies b

definition

let T be non empty pathwise_connected TopSpace;

let a, b be Point of T;

let P be Path of a,b;

for b_{1} being Path of b,a holds

( b_{1} = - P iff for t being Point of I[01] holds b_{1} . t = P . (1 - t) )

end;
let a, b be Point of T;

let P be Path of a,b;

redefine func - P means :Def3: :: BORSUK_6:def 3

for t being Point of I[01] holds it . t = P . (1 - t);

compatibility for t being Point of I[01] holds it . t = P . (1 - t);

for b

( b

proof end;

:: deftheorem Def3 defines - BORSUK_6:def 3 :

for T being non empty pathwise_connected TopSpace

for a, b being Point of T

for P being Path of a,b

for b_{5} being Path of b,a holds

( b_{5} = - P iff for t being Point of I[01] holds b_{5} . t = P . (1 - t) );

for T being non empty pathwise_connected TopSpace

for a, b being Point of T

for P being Path of a,b

for b

( b

definition

let T be non empty TopSpace;

let a, b be Point of T;

let P be Path of a,b;

let f be continuous Function of I[01],I[01];

assume that

A1: f . 0 = 0 and

A2: f . 1 = 1 and

A3: a,b are_connected ;

coherence

P * f is Path of a,b

end;
let a, b be Point of T;

let P be Path of a,b;

let f be continuous Function of I[01],I[01];

assume that

A1: f . 0 = 0 and

A2: f . 1 = 1 and

A3: a,b are_connected ;

coherence

P * f is Path of a,b

proof end;

:: deftheorem Def4 defines RePar BORSUK_6:def 4 :

for T being non empty TopSpace

for a, b being Point of T

for P being Path of a,b

for f being continuous Function of I[01],I[01] st f . 0 = 0 & f . 1 = 1 & a,b are_connected holds

RePar (P,f) = P * f;

for T being non empty TopSpace

for a, b being Point of T

for P being Path of a,b

for f being continuous Function of I[01],I[01] st f . 0 = 0 & f . 1 = 1 & a,b are_connected holds

RePar (P,f) = P * f;

theorem Th45: :: BORSUK_6:45

for T being non empty TopSpace

for a, b being Point of T

for P being Path of a,b

for f being continuous Function of I[01],I[01] st f . 0 = 0 & f . 1 = 1 & a,b are_connected holds

RePar (P,f),P are_homotopic

for a, b being Point of T

for P being Path of a,b

for f being continuous Function of I[01],I[01] st f . 0 = 0 & f . 1 = 1 & a,b are_connected holds

RePar (P,f),P are_homotopic

proof end;

theorem :: BORSUK_6:46

for T being non empty pathwise_connected TopSpace

for a, b being Point of T

for P being Path of a,b

for f being continuous Function of I[01],I[01] st f . 0 = 0 & f . 1 = 1 holds

RePar (P,f),P are_homotopic by Th45, BORSUK_2:def 3;

for a, b being Point of T

for P being Path of a,b

for f being continuous Function of I[01],I[01] st f . 0 = 0 & f . 1 = 1 holds

RePar (P,f),P are_homotopic by Th45, BORSUK_2:def 3;

definition

ex b_{1} being Function of I[01],I[01] st

for t being Point of I[01] holds

( ( t <= 1 / 2 implies b_{1} . t = 2 * t ) & ( t > 1 / 2 implies b_{1} . t = 1 ) )

for b_{1}, b_{2} being Function of I[01],I[01] st ( for t being Point of I[01] holds

( ( t <= 1 / 2 implies b_{1} . t = 2 * t ) & ( t > 1 / 2 implies b_{1} . t = 1 ) ) ) & ( for t being Point of I[01] holds

( ( t <= 1 / 2 implies b_{2} . t = 2 * t ) & ( t > 1 / 2 implies b_{2} . t = 1 ) ) ) holds

b_{1} = b_{2}
end;

func 1RP -> Function of I[01],I[01] means :Def5: :: BORSUK_6:def 5

for t being Point of I[01] holds

( ( t <= 1 / 2 implies it . t = 2 * t ) & ( t > 1 / 2 implies it . t = 1 ) );

existence for t being Point of I[01] holds

( ( t <= 1 / 2 implies it . t = 2 * t ) & ( t > 1 / 2 implies it . t = 1 ) );

ex b

for t being Point of I[01] holds

( ( t <= 1 / 2 implies b

proof end;

uniqueness for b

( ( t <= 1 / 2 implies b

( ( t <= 1 / 2 implies b

b

proof end;

:: deftheorem Def5 defines 1RP BORSUK_6:def 5 :

for b_{1} being Function of I[01],I[01] holds

( b_{1} = 1RP iff for t being Point of I[01] holds

( ( t <= 1 / 2 implies b_{1} . t = 2 * t ) & ( t > 1 / 2 implies b_{1} . t = 1 ) ) );

for b

( b

( ( t <= 1 / 2 implies b

definition

ex b_{1} being Function of I[01],I[01] st

for t being Point of I[01] holds

( ( t <= 1 / 2 implies b_{1} . t = 0 ) & ( t > 1 / 2 implies b_{1} . t = (2 * t) - 1 ) )

for b_{1}, b_{2} being Function of I[01],I[01] st ( for t being Point of I[01] holds

( ( t <= 1 / 2 implies b_{1} . t = 0 ) & ( t > 1 / 2 implies b_{1} . t = (2 * t) - 1 ) ) ) & ( for t being Point of I[01] holds

( ( t <= 1 / 2 implies b_{2} . t = 0 ) & ( t > 1 / 2 implies b_{2} . t = (2 * t) - 1 ) ) ) holds

b_{1} = b_{2}
end;

func 2RP -> Function of I[01],I[01] means :Def6: :: BORSUK_6:def 6

for t being Point of I[01] holds

( ( t <= 1 / 2 implies it . t = 0 ) & ( t > 1 / 2 implies it . t = (2 * t) - 1 ) );

existence for t being Point of I[01] holds

( ( t <= 1 / 2 implies it . t = 0 ) & ( t > 1 / 2 implies it . t = (2 * t) - 1 ) );

ex b

for t being Point of I[01] holds

( ( t <= 1 / 2 implies b

proof end;

uniqueness for b

( ( t <= 1 / 2 implies b

( ( t <= 1 / 2 implies b

b

proof end;

:: deftheorem Def6 defines 2RP BORSUK_6:def 6 :

for b_{1} being Function of I[01],I[01] holds

( b_{1} = 2RP iff for t being Point of I[01] holds

( ( t <= 1 / 2 implies b_{1} . t = 0 ) & ( t > 1 / 2 implies b_{1} . t = (2 * t) - 1 ) ) );

for b

( b

( ( t <= 1 / 2 implies b

definition

ex b_{1} being Function of I[01],I[01] st

for x being Point of I[01] holds

( ( x <= 1 / 2 implies b_{1} . x = (1 / 2) * x ) & ( x > 1 / 2 & x <= 3 / 4 implies b_{1} . x = x - (1 / 4) ) & ( x > 3 / 4 implies b_{1} . x = (2 * x) - 1 ) )

for b_{1}, b_{2} being Function of I[01],I[01] st ( for x being Point of I[01] holds

( ( x <= 1 / 2 implies b_{1} . x = (1 / 2) * x ) & ( x > 1 / 2 & x <= 3 / 4 implies b_{1} . x = x - (1 / 4) ) & ( x > 3 / 4 implies b_{1} . x = (2 * x) - 1 ) ) ) & ( for x being Point of I[01] holds

( ( x <= 1 / 2 implies b_{2} . x = (1 / 2) * x ) & ( x > 1 / 2 & x <= 3 / 4 implies b_{2} . x = x - (1 / 4) ) & ( x > 3 / 4 implies b_{2} . x = (2 * x) - 1 ) ) ) holds

b_{1} = b_{2}
end;

func 3RP -> Function of I[01],I[01] means :Def7: :: BORSUK_6:def 7

for x being Point of I[01] holds

( ( x <= 1 / 2 implies it . x = (1 / 2) * x ) & ( x > 1 / 2 & x <= 3 / 4 implies it . x = x - (1 / 4) ) & ( x > 3 / 4 implies it . x = (2 * x) - 1 ) );

existence for x being Point of I[01] holds

( ( x <= 1 / 2 implies it . x = (1 / 2) * x ) & ( x > 1 / 2 & x <= 3 / 4 implies it . x = x - (1 / 4) ) & ( x > 3 / 4 implies it . x = (2 * x) - 1 ) );

ex b

for x being Point of I[01] holds

( ( x <= 1 / 2 implies b

proof end;

uniqueness for b

( ( x <= 1 / 2 implies b

( ( x <= 1 / 2 implies b

b

proof end;

:: deftheorem Def7 defines 3RP BORSUK_6:def 7 :

for b_{1} being Function of I[01],I[01] holds

( b_{1} = 3RP iff for x being Point of I[01] holds

( ( x <= 1 / 2 implies b_{1} . x = (1 / 2) * x ) & ( x > 1 / 2 & x <= 3 / 4 implies b_{1} . x = x - (1 / 4) ) & ( x > 3 / 4 implies b_{1} . x = (2 * x) - 1 ) ) );

for b

( b

( ( x <= 1 / 2 implies b

theorem Th50: :: BORSUK_6:50

for T being non empty TopSpace

for a, b being Point of T

for P being Path of a,b

for Q being constant Path of b,b st a,b are_connected holds

RePar (P,1RP) = P + Q

for a, b being Point of T

for P being Path of a,b

for Q being constant Path of b,b st a,b are_connected holds

RePar (P,1RP) = P + Q

proof end;

theorem Th51: :: BORSUK_6:51

for T being non empty TopSpace

for a, b being Point of T

for P being Path of a,b

for Q being constant Path of a,a st a,b are_connected holds

RePar (P,2RP) = Q + P

for a, b being Point of T

for P being Path of a,b

for Q being constant Path of a,a st a,b are_connected holds

RePar (P,2RP) = Q + P

proof end;

theorem Th52: :: BORSUK_6:52

for T being non empty TopSpace

for a, b, c, d being Point of T

for P being Path of a,b

for Q being Path of b,c

for R being Path of c,d st a,b are_connected & b,c are_connected & c,d are_connected holds

RePar (((P + Q) + R),3RP) = P + (Q + R)

for a, b, c, d being Point of T

for P being Path of a,b

for Q being Path of b,c

for R being Path of c,d st a,b are_connected & b,c are_connected & c,d are_connected holds

RePar (((P + Q) + R),3RP) = P + (Q + R)

proof end;

definition

ex b_{1} being Subset of [:I[01],I[01]:] st

for x being set holds

( x in b_{1} iff ex a, b being Point of I[01] st

( x = [a,b] & b <= 1 - (2 * a) ) )

for b_{1}, b_{2} being Subset of [:I[01],I[01]:] st ( for x being set holds

( x in b_{1} iff ex a, b being Point of I[01] st

( x = [a,b] & b <= 1 - (2 * a) ) ) ) & ( for x being set holds

( x in b_{2} iff ex a, b being Point of I[01] st

( x = [a,b] & b <= 1 - (2 * a) ) ) ) holds

b_{1} = b_{2}
end;

func LowerLeftUnitTriangle -> Subset of [:I[01],I[01]:] means :Def8: :: BORSUK_6:def 8

for x being set holds

( x in it iff ex a, b being Point of I[01] st

( x = [a,b] & b <= 1 - (2 * a) ) );

existence for x being set holds

( x in it iff ex a, b being Point of I[01] st

( x = [a,b] & b <= 1 - (2 * a) ) );

ex b

for x being set holds

( x in b

( x = [a,b] & b <= 1 - (2 * a) ) )

proof end;

uniqueness for b

( x in b

( x = [a,b] & b <= 1 - (2 * a) ) ) ) & ( for x being set holds

( x in b

( x = [a,b] & b <= 1 - (2 * a) ) ) ) holds

b

proof end;

:: deftheorem Def8 defines LowerLeftUnitTriangle BORSUK_6:def 8 :

for b_{1} being Subset of [:I[01],I[01]:] holds

( b_{1} = LowerLeftUnitTriangle iff for x being set holds

( x in b_{1} iff ex a, b being Point of I[01] st

( x = [a,b] & b <= 1 - (2 * a) ) ) );

for b

( b

( x in b

( x = [a,b] & b <= 1 - (2 * a) ) ) );

definition

ex b_{1} being Subset of [:I[01],I[01]:] st

for x being set holds

( x in b_{1} iff ex a, b being Point of I[01] st

( x = [a,b] & b >= 1 - (2 * a) & b >= (2 * a) - 1 ) )

for b_{1}, b_{2} being Subset of [:I[01],I[01]:] st ( for x being set holds

( x in b_{1} iff ex a, b being Point of I[01] st

( x = [a,b] & b >= 1 - (2 * a) & b >= (2 * a) - 1 ) ) ) & ( for x being set holds

( x in b_{2} iff ex a, b being Point of I[01] st

( x = [a,b] & b >= 1 - (2 * a) & b >= (2 * a) - 1 ) ) ) holds

b_{1} = b_{2}
end;

func UpperUnitTriangle -> Subset of [:I[01],I[01]:] means :Def9: :: BORSUK_6:def 9

for x being set holds

( x in it iff ex a, b being Point of I[01] st

( x = [a,b] & b >= 1 - (2 * a) & b >= (2 * a) - 1 ) );

existence for x being set holds

( x in it iff ex a, b being Point of I[01] st

( x = [a,b] & b >= 1 - (2 * a) & b >= (2 * a) - 1 ) );

ex b

for x being set holds

( x in b

( x = [a,b] & b >= 1 - (2 * a) & b >= (2 * a) - 1 ) )

proof end;

uniqueness for b

( x in b

( x = [a,b] & b >= 1 - (2 * a) & b >= (2 * a) - 1 ) ) ) & ( for x being set holds

( x in b

( x = [a,b] & b >= 1 - (2 * a) & b >= (2 * a) - 1 ) ) ) holds

b

proof end;

:: deftheorem Def9 defines UpperUnitTriangle BORSUK_6:def 9 :

for b_{1} being Subset of [:I[01],I[01]:] holds

( b_{1} = UpperUnitTriangle iff for x being set holds

( x in b_{1} iff ex a, b being Point of I[01] st

( x = [a,b] & b >= 1 - (2 * a) & b >= (2 * a) - 1 ) ) );

for b

( b

( x in b

( x = [a,b] & b >= 1 - (2 * a) & b >= (2 * a) - 1 ) ) );

definition

ex b_{1} being Subset of [:I[01],I[01]:] st

for x being set holds

( x in b_{1} iff ex a, b being Point of I[01] st

( x = [a,b] & b <= (2 * a) - 1 ) )

for b_{1}, b_{2} being Subset of [:I[01],I[01]:] st ( for x being set holds

( x in b_{1} iff ex a, b being Point of I[01] st

( x = [a,b] & b <= (2 * a) - 1 ) ) ) & ( for x being set holds

( x in b_{2} iff ex a, b being Point of I[01] st

( x = [a,b] & b <= (2 * a) - 1 ) ) ) holds

b_{1} = b_{2}
end;

func LowerRightUnitTriangle -> Subset of [:I[01],I[01]:] means :Def10: :: BORSUK_6:def 10

for x being set holds

( x in it iff ex a, b being Point of I[01] st

( x = [a,b] & b <= (2 * a) - 1 ) );

existence for x being set holds

( x in it iff ex a, b being Point of I[01] st

( x = [a,b] & b <= (2 * a) - 1 ) );

ex b

for x being set holds

( x in b

( x = [a,b] & b <= (2 * a) - 1 ) )

proof end;

uniqueness for b

( x in b

( x = [a,b] & b <= (2 * a) - 1 ) ) ) & ( for x being set holds

( x in b

( x = [a,b] & b <= (2 * a) - 1 ) ) ) holds

b

proof end;

:: deftheorem Def10 defines LowerRightUnitTriangle BORSUK_6:def 10 :

for b_{1} being Subset of [:I[01],I[01]:] holds

( b_{1} = LowerRightUnitTriangle iff for x being set holds

( x in b_{1} iff ex a, b being Point of I[01] st

( x = [a,b] & b <= (2 * a) - 1 ) ) );

for b

( b

( x in b

( x = [a,b] & b <= (2 * a) - 1 ) ) );

theorem Th54: :: BORSUK_6:54

IBB = { p where p is Point of [:I[01],I[01]:] : ( p `2 >= 1 - (2 * (p `1)) & p `2 >= (2 * (p `1)) - 1 ) }

proof end;

registration

coherence

( IAA is closed & not IAA is empty ) by Th24, Th53;

coherence

( IBB is closed & not IBB is empty ) by Th25, Th54;

coherence

( ICC is closed & not ICC is empty ) by Th26, Th55;

end;
( IAA is closed & not IAA is empty ) by Th24, Th53;

coherence

( IBB is closed & not IBB is empty ) by Th25, Th54;

coherence

( ICC is closed & not ICC is empty ) by Th26, Th55;

Lm1: for x, y being Point of I[01] holds [x,y] in the carrier of [:I[01],I[01]:]

;

theorem Th73: :: BORSUK_6:73

for T being non empty TopSpace

for a, b, c, d being Point of T

for P being Path of a,b

for Q being Path of b,c

for R being Path of c,d st a,b are_connected & b,c are_connected & c,d are_connected holds

(P + Q) + R,P + (Q + R) are_homotopic

for a, b, c, d being Point of T

for P being Path of a,b

for Q being Path of b,c

for R being Path of c,d st a,b are_connected & b,c are_connected & c,d are_connected holds

(P + Q) + R,P + (Q + R) are_homotopic

proof end;

theorem :: BORSUK_6:74

for X being non empty pathwise_connected TopSpace

for a1, b1, c1, d1 being Point of X

for P being Path of a1,b1

for Q being Path of b1,c1

for R being Path of c1,d1 holds (P + Q) + R,P + (Q + R) are_homotopic

for a1, b1, c1, d1 being Point of X

for P being Path of a1,b1

for Q being Path of b1,c1

for R being Path of c1,d1 holds (P + Q) + R,P + (Q + R) are_homotopic

proof end;

theorem Th75: :: BORSUK_6:75

for T being non empty TopSpace

for a, b, c being Point of T

for P1, P2 being Path of a,b

for Q1, Q2 being Path of b,c st a,b are_connected & b,c are_connected & P1,P2 are_homotopic & Q1,Q2 are_homotopic holds

P1 + Q1,P2 + Q2 are_homotopic

for a, b, c being Point of T

for P1, P2 being Path of a,b

for Q1, Q2 being Path of b,c st a,b are_connected & b,c are_connected & P1,P2 are_homotopic & Q1,Q2 are_homotopic holds

P1 + Q1,P2 + Q2 are_homotopic

proof end;

theorem :: BORSUK_6:76

for X being non empty pathwise_connected TopSpace

for a1, b1, c1 being Point of X

for P1, P2 being Path of a1,b1

for Q1, Q2 being Path of b1,c1 st P1,P2 are_homotopic & Q1,Q2 are_homotopic holds

P1 + Q1,P2 + Q2 are_homotopic

for a1, b1, c1 being Point of X

for P1, P2 being Path of a1,b1

for Q1, Q2 being Path of b1,c1 st P1,P2 are_homotopic & Q1,Q2 are_homotopic holds

P1 + Q1,P2 + Q2 are_homotopic

proof end;

theorem Th77: :: BORSUK_6:77

for T being non empty TopSpace

for a, b being Point of T

for P, Q being Path of a,b st a,b are_connected & P,Q are_homotopic holds

- P, - Q are_homotopic

for a, b being Point of T

for P, Q being Path of a,b st a,b are_connected & P,Q are_homotopic holds

- P, - Q are_homotopic

proof end;

theorem :: BORSUK_6:78

for X being non empty pathwise_connected TopSpace

for a1, b1 being Point of X

for P, Q being Path of a1,b1 st P,Q are_homotopic holds

- P, - Q are_homotopic by Th77, BORSUK_2:def 3;

for a1, b1 being Point of X

for P, Q being Path of a1,b1 st P,Q are_homotopic holds

- P, - Q are_homotopic by Th77, BORSUK_2:def 3;

theorem :: BORSUK_6:79

for T being non empty TopSpace

for a, b being Point of T

for P, Q, R being Path of a,b st P,Q are_homotopic & Q,R are_homotopic holds

P,R are_homotopic

for a, b being Point of T

for P, Q, R being Path of a,b st P,Q are_homotopic & Q,R are_homotopic holds

P,R are_homotopic

proof end;

theorem Th80: :: BORSUK_6:80

for T being non empty TopSpace

for a, b being Point of T

for P being Path of a,b

for Q being constant Path of b,b st a,b are_connected holds

P + Q,P are_homotopic

for a, b being Point of T

for P being Path of a,b

for Q being constant Path of b,b st a,b are_connected holds

P + Q,P are_homotopic

proof end;

theorem :: BORSUK_6:81

for X being non empty pathwise_connected TopSpace

for a1, b1 being Point of X

for P being Path of a1,b1

for Q being constant Path of b1,b1 holds P + Q,P are_homotopic by Th80, BORSUK_2:def 3;

for a1, b1 being Point of X

for P being Path of a1,b1

for Q being constant Path of b1,b1 holds P + Q,P are_homotopic by Th80, BORSUK_2:def 3;

theorem Th82: :: BORSUK_6:82

for T being non empty TopSpace

for a, b being Point of T

for P being Path of a,b

for Q being constant Path of a,a st a,b are_connected holds

Q + P,P are_homotopic

for a, b being Point of T

for P being Path of a,b

for Q being constant Path of a,a st a,b are_connected holds

Q + P,P are_homotopic

proof end;

theorem :: BORSUK_6:83

for X being non empty pathwise_connected TopSpace

for a1, b1 being Point of X

for P being Path of a1,b1

for Q being constant Path of a1,a1 holds Q + P,P are_homotopic by Th82, BORSUK_2:def 3;

for a1, b1 being Point of X

for P being Path of a1,b1

for Q being constant Path of a1,a1 holds Q + P,P are_homotopic by Th82, BORSUK_2:def 3;

theorem Th84: :: BORSUK_6:84

for T being non empty TopSpace

for a, b being Point of T

for P being Path of a,b

for Q being constant Path of a,a st a,b are_connected holds

P + (- P),Q are_homotopic

for a, b being Point of T

for P being Path of a,b

for Q being constant Path of a,a st a,b are_connected holds

P + (- P),Q are_homotopic

proof end;

theorem :: BORSUK_6:85

for X being non empty pathwise_connected TopSpace

for a1, b1 being Point of X

for P being Path of a1,b1

for Q being constant Path of a1,a1 holds P + (- P),Q are_homotopic by Th84, BORSUK_2:def 3;

for a1, b1 being Point of X

for P being Path of a1,b1

for Q being constant Path of a1,a1 holds P + (- P),Q are_homotopic by Th84, BORSUK_2:def 3;

theorem Th86: :: BORSUK_6:86

for T being non empty TopSpace

for a, b being Point of T

for P being Path of b,a

for Q being constant Path of a,a st b,a are_connected holds

(- P) + P,Q are_homotopic

for a, b being Point of T

for P being Path of b,a

for Q being constant Path of a,a st b,a are_connected holds

(- P) + P,Q are_homotopic

proof end;

theorem :: BORSUK_6:87

for X being non empty pathwise_connected TopSpace

for a1, b1 being Point of X

for P being Path of b1,a1

for Q being constant Path of a1,a1 holds (- P) + P,Q are_homotopic by Th86, BORSUK_2:def 3;

for a1, b1 being Point of X

for P being Path of b1,a1

for Q being constant Path of a1,a1 holds (- P) + P,Q are_homotopic by Th86, BORSUK_2:def 3;

theorem :: BORSUK_6:88

for T being non empty TopSpace

for a being Point of T

for P, Q being constant Path of a,a holds P,Q are_homotopic

for a being Point of T

for P, Q being constant Path of a,a holds P,Q are_homotopic

proof end;

definition

let T be non empty TopSpace;

let a, b be Point of T;

let P, Q be Path of a,b;

assume A1: P,Q are_homotopic ;

ex b_{1} being Function of [:I[01],I[01]:],T st

( b_{1} is continuous & ( for t being Point of I[01] holds

( b_{1} . (t,0) = P . t & b_{1} . (t,1) = Q . t & b_{1} . (0,t) = a & b_{1} . (1,t) = b ) ) )
by A1;

end;
let a, b be Point of T;

let P, Q be Path of a,b;

assume A1: P,Q are_homotopic ;

mode Homotopy of P,Q -> Function of [:I[01],I[01]:],T means :: BORSUK_6:def 11

( it is continuous & ( for t being Point of I[01] holds

( it . (t,0) = P . t & it . (t,1) = Q . t & it . (0,t) = a & it . (1,t) = b ) ) );

existence ( it is continuous & ( for t being Point of I[01] holds

( it . (t,0) = P . t & it . (t,1) = Q . t & it . (0,t) = a & it . (1,t) = b ) ) );

ex b

( b

( b

:: deftheorem defines Homotopy BORSUK_6:def 11 :

for T being non empty TopSpace

for a, b being Point of T

for P, Q being Path of a,b st P,Q are_homotopic holds

for b_{6} being Function of [:I[01],I[01]:],T holds

( b_{6} is Homotopy of P,Q iff ( b_{6} is continuous & ( for t being Point of I[01] holds

( b_{6} . (t,0) = P . t & b_{6} . (t,1) = Q . t & b_{6} . (0,t) = a & b_{6} . (1,t) = b ) ) ) );

for T being non empty TopSpace

for a, b being Point of T

for P, Q being Path of a,b st P,Q are_homotopic holds

for b

( b

( b