:: Algebraic Properties of Homotopies
:: by Adam Grabowski and Artur Korni{\l}owicz
::
:: Received March 18, 2004
:: Copyright (c) 2004 Association of Mizar Users
scheme :: BORSUK_6:sch 1
ExFunc3CondD{
F1()
-> non
empty set ,
P1[
set ],
P2[
set ],
P3[
set ],
F2(
set )
-> set ,
F3(
set )
-> set ,
F4(
set )
-> set } :
ex
f being
Function st
(
dom f = F1() & ( for
c being
Element of
F1() holds
( (
P1[
c] implies
f . c = F2(
c) ) & (
P2[
c] implies
f . c = F3(
c) ) & (
P3[
c] implies
f . c = F4(
c) ) ) ) )
provided
A1:
for
c being
Element of
F1() holds
( (
P1[
c] implies not
P2[
c] ) & (
P1[
c] implies not
P3[
c] ) & (
P2[
c] implies not
P3[
c] ) )
and A2:
for
c being
Element of
F1() holds
(
P1[
c] or
P2[
c] or
P3[
c] )
theorem Th1: :: BORSUK_6:1
theorem :: BORSUK_6:2
canceled;
theorem :: BORSUK_6:3
canceled;
theorem :: BORSUK_6:4
canceled;
theorem Th5: :: BORSUK_6:5
theorem Th6: :: BORSUK_6:6
theorem Th7: :: BORSUK_6:7
theorem Th8: :: BORSUK_6:8
theorem Th9: :: BORSUK_6:9
theorem Th10: :: BORSUK_6:10
theorem :: BORSUK_6:11
canceled;
theorem Th12: :: BORSUK_6:12
theorem Th13: :: BORSUK_6:13
theorem Th14: :: BORSUK_6:14
theorem Th15: :: BORSUK_6:15
theorem Th16: :: BORSUK_6:16
theorem Th17: :: BORSUK_6:17
theorem Th18: :: BORSUK_6:18
theorem Th19: :: BORSUK_6:19
theorem Th20: :: BORSUK_6:20
theorem Th21: :: BORSUK_6:21
theorem Th22: :: BORSUK_6:22
theorem Th23: :: BORSUK_6:23
theorem Th24: :: BORSUK_6:24
theorem Th25: :: BORSUK_6:25
theorem Th26: :: BORSUK_6:26
theorem Th27: :: BORSUK_6:27
theorem Th28: :: BORSUK_6:28
theorem Th29: :: BORSUK_6:29
theorem Th30: :: BORSUK_6:30
theorem Th31: :: BORSUK_6:31
theorem Th32: :: BORSUK_6:32
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] :]
theorem Th33: :: BORSUK_6:33
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.]:]
theorem Th34: :: BORSUK_6:34
theorem Th35: :: BORSUK_6:35
theorem :: BORSUK_6:36
definition
let a,
b,
c,
d be
real number ;
canceled;func L[01] a,
b,
c,
d -> Function of
(Closed-Interval-TSpace a,b),
(Closed-Interval-TSpace c,d) equals :: BORSUK_6:def 2
(L[01] ((#) c,d),(c,d (#) )) * (P[01] a,b,((#) 0 ,1),(0 ,1 (#) ));
correctness
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;
:: deftheorem BORSUK_6:def 1 :
canceled;
:: deftheorem defines L[01] BORSUK_6:def 2 :
for
a,
b,
c,
d being
real number holds
L[01] a,
b,
c,
d = (L[01] ((#) c,d),(c,d (#) )) * (P[01] a,b,((#) 0 ,1),(0 ,1 (#) ));
theorem Th37: :: BORSUK_6:37
theorem Th38: :: BORSUK_6:38
theorem Th39: :: BORSUK_6:39
theorem Th40: :: BORSUK_6:40
theorem Th41: :: BORSUK_6:41
theorem :: BORSUK_6:42
theorem Th43: :: BORSUK_6:43
theorem Th44: :: BORSUK_6:44
theorem Th45: :: BORSUK_6:45
theorem Th46: :: BORSUK_6:46
theorem :: BORSUK_6:47
canceled;
theorem :: BORSUK_6:48
canceled;
theorem :: BORSUK_6:49
canceled;
theorem Th50: :: BORSUK_6:50
theorem :: BORSUK_6:51
:: deftheorem BORSUK_6:def 3 :
canceled;
:: deftheorem defines + BORSUK_6:def 4 :
:: deftheorem Def5 defines - BORSUK_6:def 5 :
:: deftheorem Def6 defines RePar BORSUK_6:def 6 :
theorem :: BORSUK_6:52
canceled;
theorem Th53: :: BORSUK_6:53
theorem :: BORSUK_6:54
:: deftheorem Def7 defines 1RP BORSUK_6:def 7 :
theorem Th55: :: BORSUK_6:55
:: deftheorem Def8 defines 2RP BORSUK_6:def 8 :
theorem Th56: :: BORSUK_6:56
:: deftheorem Def9 defines 3RP BORSUK_6:def 9 :
theorem Th57: :: BORSUK_6:57
theorem Th58: :: BORSUK_6:58
theorem Th59: :: BORSUK_6:59
theorem Th60: :: BORSUK_6:60
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)
definition
func LowerLeftUnitTriangle -> 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 <= 1
- (2 * a) ) );
existence
ex b1 being Subset of [:I[01] ,I[01] :] st
for x being set holds
( x in b1 iff ex a, b being Point of I[01] st
( x = [a,b] & b <= 1 - (2 * a) ) )
uniqueness
for b1, b2 being Subset of [:I[01] ,I[01] :] st ( for x being set holds
( x in b1 iff ex a, b being Point of I[01] st
( x = [a,b] & b <= 1 - (2 * a) ) ) ) & ( for x being set holds
( x in b2 iff ex a, b being Point of I[01] st
( x = [a,b] & b <= 1 - (2 * a) ) ) ) holds
b1 = b2
end;
:: deftheorem Def10 defines LowerLeftUnitTriangle BORSUK_6:def 10 :
definition
func UpperUnitTriangle -> Subset of
[:I[01] ,I[01] :] means :
Def11:
:: BORSUK_6:def 11
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
ex b1 being Subset of [:I[01] ,I[01] :] st
for x being set holds
( x in b1 iff ex a, b being Point of I[01] st
( x = [a,b] & b >= 1 - (2 * a) & b >= (2 * a) - 1 ) )
uniqueness
for b1, b2 being Subset of [:I[01] ,I[01] :] st ( for x being set holds
( x in b1 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 b2 iff ex a, b being Point of I[01] st
( x = [a,b] & b >= 1 - (2 * a) & b >= (2 * a) - 1 ) ) ) holds
b1 = b2
end;
:: deftheorem Def11 defines UpperUnitTriangle BORSUK_6:def 11 :
definition
func LowerRightUnitTriangle -> Subset of
[:I[01] ,I[01] :] means :
Def12:
:: BORSUK_6:def 12
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
ex b1 being Subset of [:I[01] ,I[01] :] st
for x being set holds
( x in b1 iff ex a, b being Point of I[01] st
( x = [a,b] & b <= (2 * a) - 1 ) )
uniqueness
for b1, b2 being Subset of [:I[01] ,I[01] :] st ( for x being set holds
( x in b1 iff ex a, b being Point of I[01] st
( x = [a,b] & b <= (2 * a) - 1 ) ) ) & ( for x being set holds
( x in b2 iff ex a, b being Point of I[01] st
( x = [a,b] & b <= (2 * a) - 1 ) ) ) holds
b1 = b2
end;
:: deftheorem Def12 defines LowerRightUnitTriangle BORSUK_6:def 12 :
theorem Th61: :: BORSUK_6:61
theorem Th62: :: BORSUK_6:62
theorem Th63: :: BORSUK_6:63
theorem Th64: :: BORSUK_6:64
theorem Th65: :: BORSUK_6:65
theorem Th66: :: BORSUK_6:66
theorem Th67: :: BORSUK_6:67
theorem Th68: :: BORSUK_6:68
theorem Th69: :: BORSUK_6:69
theorem Th70: :: BORSUK_6:70
theorem Th71: :: BORSUK_6:71
theorem Th72: :: BORSUK_6:72
theorem Th73: :: BORSUK_6:73
theorem Th74: :: BORSUK_6:74
theorem Th75: :: BORSUK_6:75
theorem Th76: :: BORSUK_6:76
theorem Th77: :: BORSUK_6:77
theorem Th78: :: BORSUK_6:78
theorem Th79: :: BORSUK_6:79
theorem Th80: :: BORSUK_6:80
Lm1:
for x, y being Point of I[01] holds [x,y] in the carrier of [:I[01] ,I[01] :]
;
theorem Th81: :: BORSUK_6:81
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
theorem :: BORSUK_6:82
theorem Th83: :: BORSUK_6:83
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
theorem :: BORSUK_6:84
theorem Th85: :: BORSUK_6:85
theorem :: BORSUK_6:86
theorem :: BORSUK_6:87
theorem Th88: :: BORSUK_6:88
theorem :: BORSUK_6:89
theorem Th90: :: BORSUK_6:90
theorem :: BORSUK_6:91
theorem Th92: :: BORSUK_6:92
theorem :: BORSUK_6:93
theorem Th94: :: BORSUK_6:94
theorem :: BORSUK_6:95
theorem :: BORSUK_6:96
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
;
mode Homotopy of
P,
Q -> Function of
[:I[01] ,I[01] :],
T means :: BORSUK_6:def 13
(
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
ex b1 being Function of [:I[01] ,I[01] :],T st
( b1 is continuous & ( for t being Point of I[01] holds
( b1 . t,0 = P . t & b1 . t,1 = Q . t & b1 . 0 ,t = a & b1 . 1,t = b ) ) )
by A1, BORSUK_2:def 7;
end;
:: deftheorem defines Homotopy BORSUK_6:def 13 :
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
b6 being
Function of
[:I[01] ,I[01] :],
T holds
(
b6 is
Homotopy of
P,
Q iff (
b6 is
continuous & ( for
t being
Point of
I[01] holds
(
b6 . t,
0 = P . t &
b6 . t,1
= Q . t &
b6 . 0 ,
t = a &
b6 . 1,
t = b ) ) ) );