:: The Fundamental Group of Convex Subspaces of TOP-REAL n
::  by Artur Korni{\l}owicz
::
:: Received April 20, 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, SUBSET_1, XBOOLE_0, CONVEX1, EUCLID, PRE_TOPC, RLTOPSP1,
      BORSUK_2, STRUCT_0, RELAT_1, TARSKI, TOPREAL1, FUNCT_1, BORSUK_1, TOPS_2,
      CARD_1, ORDINAL2, GRAPH_1, ZFMISC_1, TOPMETR, ARYTM_1, ARYTM_3, XXREAL_0,
      REAL_1, SUPINF_2, BORSUK_6, ALGSTR_1, TOPALG_1, EQREL_1, WAYBEL20,
      PARTFUN1, FINSEQ_1, MEMBERED, XXREAL_1, VALUED_1, TREAL_1, TOPALG_2,
      MEASURE5, FUNCT_2, NAT_1;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, EQREL_1, RELAT_1,
      FUNCT_1, PARTFUN1, FUNCT_2, BINOP_1, NUMBERS, XXREAL_2, XCMPLX_0,
      XREAL_0, REAL_1, STRUCT_0, PRE_TOPC, BORSUK_1, TOPS_2, TOPREAL1, TREAL_1,
      TOPMETR, RLVECT_1, RLTOPSP1, EUCLID, JORDAN2B, BORSUK_2, BORSUK_6,
      TOPALG_1, XXREAL_0, FINSEQ_1, RCOMP_1;
 constructors REAL_1, RCOMP_1, BINARITH, TOPS_2, T_0TOPSP, TOPREAL1, TREAL_1,
      JORDAN2B, BORSUK_6, TOPALG_1, CONVEX1, MONOID_0, XXREAL_2, BINOP_1;
 registrations FUNCT_2, NUMBERS, XREAL_0, STRUCT_0, PRE_TOPC, BORSUK_1, EUCLID,
      TOPMETR, BORSUK_2, TOPALG_1, ZFMISC_1, RLTOPSP1, JORDAN2B, MONOID_0,
      MEMBERED, XXREAL_2, RELSET_1, JORDAN2C;
 requirements NUMERALS, BOOLE, SUBSET, ARITHM, REAL;


begin :: Convex subspaces of TOP-REAL n

reserve n for Element of NAT,
  a, b for Real;

registration
  let n be Nat;
  cluster non empty convex for Subset of TOP-REAL n;
end;

definition
  let n be Element of NAT, T be SubSpace of TOP-REAL n;
  attr T is convex means
:: TOPALG_2:def 1

  [#]T is convex Subset of TOP-REAL n;
end;

registration
  let n be Element of NAT;
  cluster convex -> pathwise_connected for non empty SubSpace of TOP-REAL n;
end;

registration
  let n be Element of NAT;
  cluster strict non empty convex for SubSpace of TOP-REAL n;
end;

theorem :: TOPALG_2:1
  for X being non empty TopSpace, Y being non empty SubSpace of X, x1,
x2 being Point of X, y1, y2 being Point of Y, f being Path of y1,y2 st x1 = y1
  & x2 = y2 & y1,y2 are_connected holds f is Path of x1,x2;

definition
  let n be Element of NAT, T being non empty convex SubSpace of TOP-REAL n, P,
  Q be Function of I[01],T;
  func ConvexHomotopy(P,Q) -> Function of [:I[01],I[01]:], T means
:: TOPALG_2:def 2

  for
s, t being Element of I[01], a1, b1 being Point of TOP-REAL n st a1 = P.s & b1
  = Q.s holds it.(s,t) = (1-t) * a1 + t * b1;
end;

theorem :: TOPALG_2:2
  for T being non empty convex SubSpace of TOP-REAL n, a, b being
  Point of T, P, Q being Path of a,b holds P, Q are_homotopic;

registration
  let n be Element of NAT, T be non empty convex SubSpace of TOP-REAL n, a, b
  be Point of T, P, Q be Path of a,b;
  cluster -> continuous for Homotopy of P,Q;
end;

theorem :: TOPALG_2:3
  for T being non empty convex SubSpace of TOP-REAL n, a being
Point of T, C being Loop of a holds the carrier of pi_1(T,a) = { Class(EqRel(T,
  a),C) };

registration
  let n be Element of NAT, T be non empty convex SubSpace of TOP-REAL n, a be
  Point of T;
  cluster pi_1(T,a) -> trivial;
end;

begin :: Convex subspaces of R^1

theorem :: TOPALG_2:4
  |[a]|/.1 = a;

theorem :: TOPALG_2:5
  a <= b implies [.a,b.] =
  { (1-l)*a + l*b where l is Real: 0 <= l & l <= 1 };

theorem :: TOPALG_2:6
  for F being Function of [:R^1,I[01]:], R^1 st for x being Point
of R^1, i being Point of I[01] holds F.(x,i) = (1-i) * x holds F is continuous;

theorem :: TOPALG_2:7
  for F being Function of [:R^1,I[01]:], R^1 st for x being Point
  of R^1, i being Point of I[01] holds F.(x,i) = i * x holds F is continuous;

registration
  cluster non empty interval for Subset of R^1;
end;

registration
  let T be real-membered TopStruct;
  cluster interval for Subset of T;
end;

definition

  let T be real-membered TopStruct;
  attr T is interval means
:: TOPALG_2:def 3

  [#]T is interval;
end;

registration
  cluster strict non empty interval for SubSpace of R^1;
end;

definition
  redefine func R^1 -> interval SubSpace of R^1;
end;

theorem :: TOPALG_2:8
  for T being non empty interval SubSpace of R^1, a, b being Point
  of T holds [. a, b .] c= the carrier of T;

registration
  cluster interval -> pathwise_connected for non empty SubSpace of R^1;
end;

theorem :: TOPALG_2:9
  a <= b implies Closed-Interval-TSpace(a,b) is interval;

theorem :: TOPALG_2:10
  I[01] is interval;

theorem :: TOPALG_2:11
  a <= b implies Closed-Interval-TSpace(a,b) is pathwise_connected;

definition
  let T be non empty interval SubSpace of R^1, P, Q be Function of I[01],T;
  func R1Homotopy(P,Q) -> Function of [:I[01],I[01]:], T means
:: TOPALG_2:def 4

  for s, t being Element of I[01] holds it.(s,t) = (1-t) * P.s + t * Q.s;
end;

theorem :: TOPALG_2:12
  for T being non empty interval SubSpace of R^1, a, b being Point
  of T, P, Q being Path of a,b holds P, Q are_homotopic;

registration
  let T be non empty interval SubSpace of R^1, a, b be Point of T, P, Q be Path
  of a,b;
  cluster -> continuous for Homotopy of P,Q;
end;

theorem :: TOPALG_2:13
  for T being non empty interval SubSpace of R^1, a being Point of T
  , C being Loop of a holds the carrier of pi_1(T,a) = { Class(EqRel(T,a),C) };

registration
  let T be non empty interval SubSpace of R^1, a be Point of T;
  cluster pi_1(T,a) -> trivial;
end;

theorem :: TOPALG_2:14
  a <= b implies for x, y being Point of Closed-Interval-TSpace(a,b), P,
  Q being Path of x,y holds P, Q are_homotopic;

theorem :: TOPALG_2:15
  a <= b implies for x being Point of Closed-Interval-TSpace(a,b), C
  being Loop of x holds the carrier of pi_1(Closed-Interval-TSpace(a,b),x) = {
  Class(EqRel(Closed-Interval-TSpace(a,b),x),C) };

theorem :: TOPALG_2:16
  for x, y being Point of I[01], P, Q being Path of x,y holds P, Q
  are_homotopic;

theorem :: TOPALG_2:17
  for x being Point of I[01], C being Loop of x holds the carrier of
  pi_1(I[01],x) = { Class(EqRel(I[01],x),C) };

registration
  let x be Point of I[01];
  cluster pi_1(I[01],x) -> trivial;
end;

registration
  let n;
  let T be non empty convex SubSpace of TOP-REAL n, P, Q be continuous
  Function of I[01],T;
  cluster ConvexHomotopy(P,Q) -> continuous;
end;

theorem :: TOPALG_2:18
  for n being Element of NAT, T being non empty convex SubSpace of
TOP-REAL n, a, b being Point of T, P, Q being Path of a,b holds ConvexHomotopy(
  P,Q) is Homotopy of P,Q;

registration
  let T be non empty interval SubSpace of R^1, P, Q be continuous Function of
  I[01],T;
  cluster R1Homotopy(P,Q) -> continuous;
end;

theorem :: TOPALG_2:19
  for T being non empty interval SubSpace of R^1, a, b be Point of T, P, Q
  be Path of a,b holds R1Homotopy(P,Q) is Homotopy of P,Q;