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