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