:: Algebraic Properties of Homotopies
:: by Adam Grabowski and Artur Korni{\l}owicz
::
:: Received March 18, 2004
:: Copyright (c) 2004-2021 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, XBOOLE_0, FUNCT_1, RELAT_1, SUBSET_1, STRUCT_0,
ZFMISC_1, BORSUK_1, XXREAL_1, CARD_1, XREAL_0, XXREAL_0, ARYTM_1,
ARYTM_3, TOPMETR, PRE_TOPC, GRAPH_1, RCOMP_1, TARSKI, EUCLID, MCART_1,
JGRAPH_2, FUNCT_2, MEMBERED, REAL_1, FINSEQ_1, FINSEQ_2, TOPS_2, TREAL_1,
VALUED_1, ORDINAL2, BORSUK_2, FUNCOP_1, FUNCT_4, BORSUK_6;
notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, XFAMILY, SUBSET_1, ORDINAL1,
NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, REAL_1, MEMBERED, MCART_1,
FINSEQ_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_3, FUNCT_2,
FINSEQ_2, STRUCT_0, PRE_TOPC, EUCLID, TOPS_2, RCOMP_1, COMPTS_1,
JGRAPH_2, TREAL_1, FUNCT_4, BORSUK_1, TOPMETR, BINOP_1, BORSUK_2;
constructors REAL_1, RCOMP_1, FINSEQ_4, CONNSP_1, TOPS_2, COMPTS_1, GRCAT_1,
T_0TOPSP, MONOID_0, TREAL_1, BORSUK_2, JGRAPH_2, FUNCOP_1, COMPLEX1,
PCOMPS_1, XTUPLE_0, FUNCT_4, XFAMILY;
registrations XBOOLE_0, RELSET_1, FUNCT_2, NUMBERS, XXREAL_0, XREAL_0,
MEMBERED, STRUCT_0, PRE_TOPC, BORSUK_1, MONOID_0, EUCLID, TOPMETR,
BORSUK_2, BORSUK_3, JGRAPH_2, TOPS_1, COMPTS_1, SUBSET_1, ZFMISC_1,
RELAT_1, XTUPLE_0, ORDINAL1;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
begin :: Preliminaries
scheme :: BORSUK_6:sch 1
ExFunc3CondD { C() -> non empty set, P,Q,R[set], F,G,H(set) -> set }: ex f
being Function st dom f = C() & for c being Element of C() holds (P[c] implies
f.c = F(c)) & (Q[c] implies f.c = G(c)) & (R[c] implies f.c = H(c))
provided
for c being Element of C() holds (P[c] implies not Q[c]) & (P[c]
implies not R[c]) & (Q[c] implies not R[c]) and
for c being Element of C() holds P[c] or Q[c] or R[c];
theorem :: BORSUK_6:1
the carrier of [:I[01],I[01]:] = [:[.0,1.], [.0,1.]:];
theorem :: 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);
theorem :: BORSUK_6:3
for x being Point of I[01] st x <= 1/2 holds 2 * x is Point of I[01];
theorem :: BORSUK_6:4
for x being Point of I[01] st x >= 1/2 holds 2 * x - 1 is Point of I[01];
theorem :: BORSUK_6:5
for p, q being Point of I[01] holds p * q is Point of I[01];
theorem :: BORSUK_6:6
for x being Point of I[01] holds 1/2 * x is Point of I[01];
theorem :: BORSUK_6:7
for x being Point of I[01] st x >= 1/2 holds x - 1/4 is Point of I[01];
theorem :: BORSUK_6:8
id I[01] is Path of 0[01], 1[01];
theorem :: BORSUK_6:9
for a, b, c, d being Point of I[01] st a <= b & c <= d holds [:
[.a,b.], [.c,d.]:] is compact non empty Subset of [:I[01], I[01]:];
begin :: Affine Maps
theorem :: 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;
theorem :: 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;
theorem :: 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;
theorem :: 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;
begin :: Real-membered Structures
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;
registration
cluster non empty real-membered for 1-sorted;
cluster non empty real-membered for TopSpace;
end;
registration
let T be real-membered 1-sorted;
cluster -> real for Element of T;
end;
registration
let T be real-membered TopStruct;
cluster -> real-membered for SubSpace of T;
end;
registration
let S, T be real-membered non empty TopSpace, p be Element of [:S, T:];
cluster p`1 -> real;
cluster p`2 -> real;
end;
registration
let T be non empty SubSpace of [:I[01], I[01]:], x be Point of T;
cluster x`1 -> real;
cluster x`2 -> real;
end;
begin :: Closed Subsets of TOP-REAL 2
theorem :: BORSUK_6:15
{p where p is Point of TOP-REAL 2 : p`2 <= 2 * p`1 - 1 } is
closed Subset of TOP-REAL 2;
theorem :: BORSUK_6:16
{p where p is Point of TOP-REAL 2 : p`2 >= 2 * p`1 - 1 } is
closed Subset of TOP-REAL 2;
theorem :: BORSUK_6:17
{p where p is Point of TOP-REAL 2 : p`2 <= 1 - 2 * p`1 } is
closed Subset of TOP-REAL 2;
theorem :: BORSUK_6:18
{p where p is Point of TOP-REAL 2 : p`2 >= 1 - 2 * p`1 } is
closed Subset of TOP-REAL 2;
theorem :: 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;
theorem :: BORSUK_6:20
ex f being Function of [:R^1,R^1:], TOP-REAL 2 st for x, y being
Real holds f. [x,y] = <*x,y*>;
theorem :: BORSUK_6:21
{ p where p is Point of [:R^1,R^1:] : p`2 <= 1 - 2 * (p`1) } is
closed Subset of [:R^1,R^1:];
theorem :: BORSUK_6:22
{ p where p is Point of [:R^1,R^1:] : p`2 <= 2 * (p`1) - 1 } is
closed Subset of [:R^1,R^1:];
theorem :: 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:];
theorem :: BORSUK_6:24
{ p where p is Point of [:I[01],I[01]:] : p`2 <= 1 - 2 * (p`1) }
is closed non empty Subset of [:I[01],I[01]:];
theorem :: 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 closed non empty Subset of [:I[01],I[01]:];
theorem :: BORSUK_6:26
{ p where p is Point of [:I[01],I[01]:] : p`2 <= 2 * (p`1) - 1 }
is closed non empty Subset of [:I[01],I[01]:];
theorem :: BORSUK_6:27
for S, T being non empty TopSpace, p being Point of [:S, T:]
holds p`1 is Point of S & p`2 is Point of T;
theorem :: 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]:];
theorem :: 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.] :];
begin :: Compact Spaces
registration
let T be TopStruct;
cluster empty compact for Subset of T;
end;
theorem :: BORSUK_6:30
for T being TopStruct holds {} is empty compact Subset of T;
theorem :: BORSUK_6:31
for T being TopStruct, a, b being Real st a > b holds [.a
,b.] is empty compact Subset of T;
theorem :: BORSUK_6:32
for a, b, c, d being Point of I[01] holds [:[.a,b.], [.c,d.]:] is
compact Subset of [:I[01], I[01]:];
begin :: Continuous Maps
definition
let a, b, c, d be Real;
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)(#));
end;
theorem :: 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;
theorem :: 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);
theorem :: BORSUK_6:35
for a, b, c, d being Real st a < b & c <= d for x being
Real st a <= x & x <= b holds L[01](a,b,c,d).x = ((d - c)/(b - a)) * (x
- a) + c;
theorem :: 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]:],r1,r2 being Real st f1.p=r1 &
f2.p=r2 holds g.p=r1*r2) & g is continuous;
theorem :: 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]:],r1,r2 being Real st f1.p=r1 &
f2.p=r2 holds g.p=r1+r2) & g is continuous;
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]:],r1,r2 being Real st f1.p=r1 & f2.p=r2
holds g.p=r1-r2) & g is continuous;
begin :: Paths
reserve T for non empty TopSpace,
a, b, c, d for Point of T;
theorem :: BORSUK_6:39
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;
theorem :: BORSUK_6:40
for X being non empty TopStruct, a, b being Point of X, 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;
theorem :: BORSUK_6:41
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;
definition
let T be non empty TopSpace, a,b be Point of T;
redefine pred a,b are_connected;
reflexivity;
symmetry;
end;
theorem :: BORSUK_6:42
a,b are_connected & b,c are_connected implies a,c are_connected;
theorem :: BORSUK_6:43
a,b are_connected implies for A being Path of a,b holds A = --A;
theorem :: BORSUK_6:44
for T being non empty pathwise_connected TopSpace, a, b being Point of
T for A being Path of a,b holds A = --A;
begin :: Reexamination of a Path Concept
definition
let T be non empty pathwise_connected TopSpace;
let a, b, c be Point of T;
let P be Path of a, b, 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) );
end;
definition
let T be non empty pathwise_connected TopSpace;
let a, b be Point of T;
let P be Path of a, b;
redefine func - P means
:: BORSUK_6:def 3
for t being Point of I[01] holds it.t = P.(1-t);
end;
begin :: Reparametrizations
definition
let T be non empty TopSpace, 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
f.0 = 0 and
f.1 = 1 and
a, b are_connected;
func RePar (P, f) -> Path of a, b equals
:: BORSUK_6:def 4
P * f;
end;
theorem :: BORSUK_6:45
for P being Path of a, b, 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;
theorem :: BORSUK_6:46
for T being non empty pathwise_connected TopSpace, a, b be Point of T,
P being Path of a, b, f being continuous Function of I[01], I[01] st f.0 = 0 &
f.1 = 1 holds RePar (P, f), P are_homotopic;
definition
func 1RP -> Function of I[01], I[01] means
:: 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);
end;
registration
cluster 1RP -> continuous;
end;
theorem :: BORSUK_6:47
1RP.0 = 0 & 1RP.1 = 1;
definition
func 2RP -> Function of I[01], I[01] means
:: 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);
end;
registration
cluster 2RP -> continuous;
end;
theorem :: BORSUK_6:48
2RP.0 = 0 & 2RP.1 = 1;
definition
func 3RP -> Function of I[01], I[01] means
:: 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);
end;
registration
cluster 3RP -> continuous;
end;
theorem :: BORSUK_6:49
3RP.0 = 0 & 3RP.1 = 1;
theorem :: BORSUK_6:50
for P being Path of a, b, Q being constant Path of b, b st a,b
are_connected holds RePar (P, 1RP) = P + Q;
theorem :: BORSUK_6:51
for P being Path of a, b, Q being constant Path of a, a st a,b
are_connected holds RePar (P, 2RP) = Q + P;
theorem :: BORSUK_6:52
for P being Path of a, b, Q being Path of b, c, 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);
begin :: Decomposition of the Unit Square
definition
func LowerLeftUnitTriangle -> Subset of [:I[01], I[01]:] means
:: 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;
end;
notation
synonym IAA for LowerLeftUnitTriangle;
end;
definition
func UpperUnitTriangle -> Subset of [:I[01], I[01]:] means
:: 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;
end;
notation
synonym IBB for UpperUnitTriangle;
end;
definition
func LowerRightUnitTriangle -> Subset of [:I[01], I[01]:] means
:: 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;
end;
notation
synonym ICC for LowerRightUnitTriangle;
end;
theorem :: BORSUK_6:53
IAA = { p where p is Point of [:I[01], I[01]:] : p`2 <= 1 - 2 * (p`1) };
theorem :: 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 };
theorem :: BORSUK_6:55
ICC = { p where p is Point of [:I[01], I[01]:] : p`2 <= 2 * (p`1 ) - 1 };
registration
cluster IAA -> closed non empty;
cluster IBB -> closed non empty;
cluster ICC -> closed non empty;
end;
theorem :: BORSUK_6:56
IAA \/ IBB \/ ICC = [:[.0,1.], [.0,1.]:];
theorem :: BORSUK_6:57
IAA /\ IBB = { p where p is Point of [:I[01], I[01]:] : p`2 = 1 - 2 * (p`1) }
;
theorem :: BORSUK_6:58
ICC /\ IBB = { p where p is Point of [:I[01], I[01]:] : p`2 = 2 * (p`1) - 1 }
;
theorem :: BORSUK_6:59
for x being Point of [:I[01], I[01]:] st x in IAA holds x`1 <= 1 /2;
theorem :: BORSUK_6:60
for x being Point of [:I[01], I[01]:] st x in ICC holds x`1 >= 1 /2;
theorem :: BORSUK_6:61
for x being Point of I[01] holds [0,x] in IAA;
theorem :: BORSUK_6:62
for s being set holds [0,s] in IBB implies s = 1;
theorem :: BORSUK_6:63
for s being set holds [s,1] in ICC implies s = 1;
theorem :: BORSUK_6:64
[0,1] in IBB;
theorem :: BORSUK_6:65
for x being Point of I[01] holds [x,1] in IBB;
theorem :: BORSUK_6:66
[1/2,0] in ICC & [1,1] in ICC;
theorem :: BORSUK_6:67
[1/2,0] in IBB;
theorem :: BORSUK_6:68
for x being Point of I[01] holds [1,x] in ICC;
theorem :: BORSUK_6:69
for x being Point of I[01] st x >= 1/2 holds [x,0] in ICC;
theorem :: BORSUK_6:70
for x being Point of I[01] st x <= 1/2 holds [x,0] in IAA;
theorem :: BORSUK_6:71
for x being Point of I[01] st x < 1/2 holds not [x,0] in IBB &
not [x,0] in ICC;
theorem :: BORSUK_6:72
IAA /\ ICC = { [1/2,0] };
begin :: Properties of a Homotopy
reserve X for non empty pathwise_connected TopSpace,
a1, b1, c1, d1 for Point of X;
theorem :: BORSUK_6:73
for P be Path of a, b, Q be Path of b, c, R be 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:74
for P be Path of a1, b1, Q be Path of b1, c1, R be Path of c1, d1
holds (P + Q) + R, P + (Q + R) are_homotopic;
theorem :: BORSUK_6:75
for P1, P2 being Path of a, b, 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:76
for P1, P2 being Path of a1, b1, Q1, Q2 being Path of b1, c1 st P1, P2
are_homotopic & Q1, Q2 are_homotopic holds P1 + Q1, P2 + Q2 are_homotopic;
theorem :: BORSUK_6:77
for P, Q being Path of a, b st a, b are_connected & P, Q
are_homotopic holds -P, -Q are_homotopic;
theorem :: BORSUK_6:78
for P, Q being Path of a1, b1 st P, Q are_homotopic holds -P, -Q
are_homotopic;
theorem :: BORSUK_6:79
for P, Q, R be Path of a, b holds P, Q are_homotopic & Q, R
are_homotopic implies P, R are_homotopic;
theorem :: BORSUK_6:80
for P be Path of a, b, Q be constant Path of b, b st a, b
are_connected holds P + Q, P are_homotopic;
theorem :: BORSUK_6:81
for P be Path of a1, b1, Q be constant Path of b1, b1 holds P + Q, P
are_homotopic;
theorem :: BORSUK_6:82
for P be Path of a, b, Q be constant Path of a, a st a, b
are_connected holds Q + P, P are_homotopic;
theorem :: BORSUK_6:83
for P be Path of a1, b1, Q be constant Path of a1, a1 holds Q + P, P
are_homotopic;
theorem :: BORSUK_6:84
for P being Path of a, b, Q being constant Path of a, a st a, b
are_connected holds P + - P, Q are_homotopic;
theorem :: BORSUK_6:85
for P being Path of a1, b1, Q being constant Path of a1, a1 holds P +
- P, Q are_homotopic;
theorem :: BORSUK_6:86
for P being Path of b, a, Q being constant Path of a, a st b, a
are_connected holds - P + P, Q are_homotopic;
theorem :: BORSUK_6:87
for P being Path of b1, a1, Q being constant Path of a1, a1 holds - P
+ P, Q are_homotopic;
theorem :: BORSUK_6:88
for P, Q be constant Path of a, a holds P, Q are_homotopic;
definition
let T be non empty TopSpace;
let a, b be Point of T;
let P, Q be Path of a, b;
assume
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;
end;