:: The Fundamental Group of Convex Subspaces of TOP-REAL n
:: by Artur Korni{\l}owicz
::
:: Received April 20, 2004
:: Copyright (c) 2004-2026 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;
definitions TARSKI, XBOOLE_0, BORSUK_2, BORSUK_6;
equalities XBOOLE_0, BINOP_1, STRUCT_0, BORSUK_1, RLTOPSP1, TOPALG_1;
expansions XBOOLE_0, BORSUK_2;
theorems XREAL_0, TARSKI, FUNCT_2, TSEP_1, PRE_TOPC, EUCLID, TOPS_2, BORSUK_1,
TOPALG_1, EQREL_1, BORSUK_2, BINOP_1, TOPMETR, JORDAN1, TOPREAL1,
FUNCT_3, BORSUK_6, JGRAPH_2, FUNCT_1, JORDAN2B, FINSEQ_4, RVSUM_1,
TREAL_1, XCMPLX_1, XREAL_1, JGRAPH_6, XXREAL_0, XXREAL_1, FINSEQ_1,
XXREAL_2, RLVECT_1, RLVECT_4;
schemes BINOP_1;
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;
existence
proof
set a = the Point of TOP-REAL n;
take LSeg(a,a);
thus thesis;
end;
end;
definition
let n be Element of NAT, T be SubSpace of TOP-REAL n;
attr T is convex means
:Def1:
[#]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;
coherence
proof
let T be non empty SubSpace of TOP-REAL n;
assume
A1: [#]T is convex Subset of TOP-REAL n;
let a, b be Point of T;
A2: the carrier of T is Subset of TOP-REAL n by TSEP_1:1;
a in the carrier of T & b in the carrier of T;
then reconsider a1 = a, b1 = b as Point of TOP-REAL n by A2;
per cases;
suppose
A3: a1 <> b1;
[#]((TOP-REAL n)|LSeg(a1,b1)) = LSeg(a1,b1) by PRE_TOPC:def 5;
then
A4: the carrier of (TOP-REAL n)|LSeg(a1,b1) c= the carrier of T by A1,
JORDAN1:def 1;
then
A5: (TOP-REAL n)|LSeg(a1,b1) is SubSpace of T by TSEP_1:4;
LSeg(a1,b1) is_an_arc_of a1,b1 by A3,TOPREAL1:9;
then consider
h being Function of I[01], (TOP-REAL n)|LSeg(a1,b1) such that
A6: h is being_homeomorphism and
A7: h.0 = a1 & h.1 = b1 by TOPREAL1:def 1;
reconsider f = h as Function of I[01], T by A4,FUNCT_2:7;
take f;
h is continuous by A6,TOPS_2:def 5;
hence f is continuous by A5,PRE_TOPC:26;
thus thesis by A7;
end;
suppose
a1 = b1;
hence a,b are_connected;
end;
end;
end;
registration
let n be Element of NAT;
cluster strict non empty convex for SubSpace of TOP-REAL n;
existence
proof
the TopStruct of TOP-REAL n is SubSpace of the TopStruct of TOP-REAL n
by TSEP_1:2;
then reconsider
T = the TopStruct of TOP-REAL n as SubSpace of TOP-REAL n by PRE_TOPC:35;
take T;
thus T is strict non empty;
[#]TOP-REAL n = [#]the TopStruct of TOP-REAL n;
hence [#]T is convex Subset of TOP-REAL n;
end;
end;
theorem
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
proof
let X be non empty TopSpace, Y be non empty SubSpace of X, x1, x2 be Point
of X, y1, y2 be Point of Y, f be Path of y1,y2 such that
A1: x1 = y1 & x2 = y2 and
A2: y1, y2 are_connected;
the carrier of Y is Subset of X by TSEP_1:1;
then reconsider g = f as Function of I[01], X by FUNCT_2:7;
f is continuous by A2,BORSUK_2:def 2;
then
A3: g is continuous by PRE_TOPC:26;
A4: g.0 = x1 & g.1 =x2 by A1,A2,BORSUK_2:def 2;
then x1, x2 are_connected by A3;
hence thesis by A4,A3,BORSUK_2:def 2;
end;
set I = the carrier of I[01];
Lm1: the carrier of [:I[01],I[01]:] = [:I,I:] by BORSUK_1:def 2;
Lm2: the carrier of [:TOP-REAL 1,I[01]:] = [:the carrier of TOP-REAL 1,I:] by
BORSUK_1:def 2;
Lm3: the carrier of [:R^1,I[01]:] = [:the carrier of R^1,I:] by BORSUK_1:def 2;
Lm4: dom id I[01] = I by FUNCT_2:def 1;
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
:Def2:
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;
existence
proof
defpred P[Element of I,Element of I,set] means ex a1, b1 being Point of
TOP-REAL n st a1 = P.$1 & b1 = Q.$1 & $3 = (1-$2) * a1 + $2 * b1;
A1: for x, y being Element of I ex z being Element of T st P[x,y,z]
proof
let x, y be Element of I;
A2: the carrier of T is Subset of TOP-REAL n by TSEP_1:1;
P.x in the carrier of T & Q.x in the carrier of T;
then reconsider a1 = P.x, b1 = Q.x as Point of TOP-REAL n by A2;
set z = (1-y) * a1 + y * b1;
A3: y <= 1 by BORSUK_1:43;
[#]T is convex Subset of TOP-REAL n by Def1;
then
A4: LSeg(a1,b1) c= [#]T by JORDAN1:def 1;
y is Real & 0 <= y by BORSUK_1:43;
then z in LSeg(a1,b1) by A3;
hence thesis by A4;
end;
consider F being Function of [:I,I:],the carrier of T such that
A5: for x, y being Element of I holds P[x,y,F.(x,y)] from BINOP_1:sch
3(A1);
reconsider F as Function of [:I[01],I[01]:], T by Lm1;
take F;
let x, y be Element of I;
ex a1, b1 being Point of TOP-REAL n st a1 = P.x & b1 = Q.x & F.(x,y)
= (1-y) * a1 + y * b1 by A5;
hence thesis;
end;
uniqueness
proof
let f, g be Function of [:I[01],I[01]:], T such that
A6: for s, t being Element of I[01], a1, b1 being Point of TOP-REAL n
st a1 = P.s & b1 = Q.s holds f.(s,t) = (1-t) * a1 + t * b1 and
A7: for s, t being Element of I[01], a1, b1 being Point of TOP-REAL n
st a1 = P.s & b1 = Q.s holds g.(s,t) = (1-t) * a1 + t * b1;
for s, t being Element of I holds f.(s,t) = g.(s,t)
proof
let s, t be Element of I;
reconsider a1 = P.s, b1 = Q.s as Point of TOP-REAL n by PRE_TOPC:25;
f.(s,t) = (1-t) * a1 + t * b1 by A6;
hence thesis by A7;
end;
hence f = g by Lm1,BINOP_1:2;
end;
end;
Lm5: for T being non empty convex SubSpace of TOP-REAL n, P, Q being
continuous Function of I[01],T holds ConvexHomotopy(P,Q) is continuous
proof
let T be non empty convex SubSpace of TOP-REAL n, P, Q be continuous
Function of I[01],T;
set F = ConvexHomotopy(P,Q);
A1: the carrier of T is Subset of TOP-REAL n by TSEP_1:1;
then reconsider G = F as Function of [:I[01],I[01]:],TOP-REAL n by FUNCT_2:7;
reconsider P1 = P, Q1 = Q as Function of I[01],TOP-REAL n by A1,FUNCT_2:7;
set E = the carrier of TOP-REAL n;
set PI = [:P,id I[01]:];
set QI = [:Q,id I[01]:];
reconsider P1, Q1 as continuous Function of I[01],TOP-REAL n by PRE_TOPC:26;
set P1I = [:P1,id I[01]:];
set Q1I = [:Q1,id I[01]:];
deffunc Fb(Element of E,Element of I) = $2*$1;
deffunc Fa(Element of E,Element of I) = (1-$2)*$1;
consider Pa being Function of [:E,I:],E such that
A2: for x being Element of E, i being Element of I holds Pa.(x,i) = Fa(x
,i) from BINOP_1:sch 4;
consider Pb being Function of [:E,I:],E such that
A3: for x being Element of E, i being Element of I holds Pb.(x,i) = Fb(x
,i) from BINOP_1:sch 4;
the carrier of [:TOP-REAL n,I[01]:] = [:E,I:] by BORSUK_1:def 2;
then reconsider Pa, Pb as Function of [:TOP-REAL n,I[01]:],TOP-REAL n;
A4: Pb is continuous by A3,TOPALG_1:18;
Pa is continuous by A2,TOPALG_1:17;
then consider g being Function of [:I[01],I[01]:],TOP-REAL n such that
A5: for r being Point of [:I[01],I[01]:] holds g.r = (Pa*P1I).r + (Pb*
Q1I).r and
A6: g is continuous by A4,JGRAPH_6:12;
A7: for p being Point of [:I[01],I[01]:] holds G.p = (Pa*P1I).p + (Pb*Q1I).p
proof
A8: dom Q = I by FUNCT_2:def 1;
A9: dom P = I by FUNCT_2:def 1;
let p be Point of [:I[01],I[01]:];
consider s, t being Point of I[01] such that
A10: p = [s,t] by BORSUK_1:10;
reconsider a1 = P.s, b1 = Q.s as Point of TOP-REAL n by PRE_TOPC:25;
A11: F.(s,t) = (1-t) * a1 + t * b1 by Def2;
A12: (id I[01]).t = t by FUNCT_1:18;
A13: (Pb*QI).p = Pb.(QI.(s,t)) by A10,FUNCT_2:15
.= Pb.(Q.s,t) by A8,A12,Lm4,FUNCT_3:def 8
.= t * Q1.s by A3;
(Pa*PI).p = Pa.(PI.(s,t)) by A10,FUNCT_2:15
.= Pa.(P.s,t) by A9,A12,Lm4,FUNCT_3:def 8
.= (1-t) * P1.s by A2;
hence thesis by A10,A13,A11;
end;
for p being Point of [:I[01],I[01]:] holds G.p = g.p
proof
let p be Point of [:I[01],I[01]:];
thus G.p = (Pa*P1I).p + (Pb*Q1I).p by A7
.= g.p by A5;
end;
hence thesis by A6,FUNCT_2:63,PRE_TOPC:27;
end;
Lm6: 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 for s being Point of I[01] holds ConvexHomotopy
(P,Q).(s,0) = P.s & ConvexHomotopy(P,Q).(s,1) = Q.s & for t being Point of
I[01] holds ConvexHomotopy(P,Q).(0,t) = a & ConvexHomotopy(P,Q).(1,t) = b
proof
reconsider x0 = 0, x1 = 1 as Point of I[01] by BORSUK_1:def 14,def 15;
let T be non empty convex SubSpace of TOP-REAL n, a, b be Point of T, P, Q
be Path of a,b;
set F = ConvexHomotopy(P,Q);
let s be Point of I[01];
reconsider a1 = P.s, b1 = Q.s as Point of TOP-REAL n by PRE_TOPC:25;
A1: P.x0 = a by BORSUK_2:def 4;
F.(s,x0) = (1-x0) * a1 + x0 * b1 by Def2;
hence F.(s,0) = a1 + 0 * b1 by RLVECT_1:def 8
.= a1 + 0.TOP-REAL n by RLVECT_1:10
.= P.s by RLVECT_1:4;
F.(s,x1) = (1-x1) * a1 + x1 * b1 by Def2;
hence F.(s,1) = 0.TOP-REAL n + 1 * b1 by RLVECT_1:10
.= 0.TOP-REAL n + b1 by RLVECT_1:def 8
.= Q.s by RLVECT_1:4;
reconsider a1 = P.x0, b1 = Q.x0 as Point of TOP-REAL n by PRE_TOPC:25;
let t be Point of I[01];
F.(0,t) = (1-t) * a1 + t * b1 & Q.x0 = a by Def2,BORSUK_2:def 4;
hence F.(0,t) = 1*a1 - t*a1 + t*a1 by A1,RLVECT_1:35
.= 1*a1 by RLVECT_4:1
.= a by A1,RLVECT_1:def 8;
A2: Q.x1 = b by BORSUK_2:def 4;
reconsider a1 = P.x1, b1 = Q.x1 as Point of TOP-REAL n by PRE_TOPC:25;
A3: P.x1 = b by BORSUK_2:def 4;
F.(1,t) = (1-t) * a1 + t * b1 by Def2;
hence F.(1,t) = 1*a1 - t*b1 + t*a1 by A3,A2,RLVECT_1:35
.= 1*b1 by A3,A2,RLVECT_4:1
.= b by A2,RLVECT_1:def 8;
end;
theorem Th2:
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
proof
let T be non empty convex SubSpace of TOP-REAL n, a, b be Point of T, P, Q
be Path of a,b;
take F = ConvexHomotopy(P,Q);
thus F is continuous by Lm5;
thus thesis by Lm6;
end;
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;
coherence
proof
let F be Homotopy of P,Q;
P, Q are_homotopic by Th2;
hence thesis by BORSUK_6:def 11;
end;
end;
theorem Th3:
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) }
proof
let T be non empty convex SubSpace of TOP-REAL n, a be Point of T, C be Loop
of a;
set E = EqRel(T,a);
hereby
let x be object;
assume x in the carrier of pi_1(T,a);
then consider P being Loop of a such that
A1: x = Class(E,P) by TOPALG_1:47;
P,C are_homotopic by Th2;
then x = Class(E,C) by A1,TOPALG_1:46;
hence x in { Class(E,C) } by TARSKI:def 1;
end;
let x be object;
assume x in { Class(E,C) };
then
A2: x = Class(E,C) by TARSKI:def 1;
C in Loops a by TOPALG_1:def 1;
then x in Class E by A2,EQREL_1:def 3;
hence thesis by TOPALG_1:def 5;
end;
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;
coherence
proof
set C = the constant Loop of a;
set E = EqRel(T,a);
the carrier of pi_1(T,a) = Class E by TOPALG_1:def 5;
then { Class(E,C) } = Class E by Th3;
hence thesis by TOPALG_1:def 5;
end;
end;
begin :: Convex subspaces of R^1
theorem Th4:
|[a]|/.1 = a
proof
reconsider y = a as Element of REAL by XREAL_0:def 1;
thus |[a]|/.1 = <*y*>/.1 .= a by FINSEQ_4:16;
end;
theorem
a <= b implies [.a,b.] =
{ (1-l)*a + l*b where l is Real: 0 <= l & l <= 1 }
proof
set X = {(1-l)*a+l*b where l is Real: 0 <= l & l <= 1};
assume
A1: a <= b;
hereby
let x be object;
assume
A2: x in [.a,b.];
then reconsider y = x as Real;
A3: a <= y & y <= b by A2,XXREAL_1:1;
per cases by A1,XXREAL_0:1;
suppose
a < b;
then
A4: b-a > b-b by XREAL_1:15;
reconsider l = (y-a)/(b-a) as Real;
l in the carrier of Closed-Interval-TSpace (0,1) by A3,BORSUK_6:2;
then l in [.0,1.] by TOPMETR:18;
then
A5: 0 <= l & l <= 1 by XXREAL_1:1;
(1-l)*a+l*b = a+l*(b-a) .= a+(y-a) by A4,XCMPLX_1:87
.= y;
hence x in X by A5;
end;
suppose
a = b;
then (1-1)*a+1*b = y by A3,XXREAL_0:1;
hence x in X;
end;
end;
let x be object;
assume x in X;
then consider l being Real such that
A6: x = (1-l)*a+l*b and
A7: 0 <= l & l <= 1;
a <= (1-l)*a+l*b & (1-l)*a+l*b <= b by A1,A7,XREAL_1:172,173;
hence thesis by A6,XXREAL_1:1;
end;
theorem Th6:
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
proof
deffunc Fa(Element of TOP-REAL 1, Element of I) = (1-$2)*$1;
consider G being Function of [:the carrier of TOP-REAL 1,I:], the carrier of
TOP-REAL 1 such that
A1: for x being Point of TOP-REAL 1, i being Point of I[01] holds G.(x,i
) = Fa(x,i) from BINOP_1:sch 4;
reconsider G as Function of [:TOP-REAL 1,I[01]:], TOP-REAL 1 by Lm2;
consider f being Function of TOP-REAL 1,R^1 such that
A2: for p being Element of TOP-REAL 1 holds f.p = p/.1 by JORDAN2B:1;
A3: f is being_homeomorphism by A2,JORDAN2B:28;
then
A4: f is continuous by TOPS_2:def 5;
let F be Function of [:R^1,I[01]:], R^1 such that
A5: for x being Point of R^1, i being Point of I[01] holds F.(x,i) = (1-
i) * x;
A6: for x being Point of [:R^1,I[01]:] holds F.x = (f*(G*[:f",id I[01]:])).x
proof
reconsider ff = f as Function;
let x be Point of [:R^1,I[01]:];
consider a being Point of R^1, b being Point of I[01] such that
A7: x = [a,b] by BORSUK_1:10;
A8: dom (f") = the carrier of R^1 by FUNCT_2:def 1;
rng f = [#]R^1 by A3,TOPS_2:def 5;
then
A9: f is onto by FUNCT_2:def 3;
A10: dom f = the carrier of TOP-REAL 1 by FUNCT_2:def 1;
set g = ff";
consider z being Real such that
A11: (1-b)*f".a = <*z*> by JORDAN2B:20;
reconsider zz=z as Element of REAL by XREAL_0:def 1;
A12: <*a*> = |[a]|;
then reconsider w = <*a*> as Element of REAL 1 by EUCLID:22;
A13: ff is one-to-one by A3,TOPS_2:def 5;
f.<*a*> = |[a]|/.1 by A2
.= a by Th4;
then <*a*> = g.a by A10,A13,A12,FUNCT_1:32;
then
A14: w = f/".a by A9,A13,TOPS_2:def 4;
A15: <*z*> = (1-b)*(f/".a) by A11
.= (1-b)*w by A14
.= <*(1-b)*a*> by RVSUM_1:47;
thus (f*(G*[:f",id I[01]:])).x = f.((G*[:f",id I[01]:]).x) by FUNCT_2:15
.= f.(G.([:f",id I[01]:].(a,b))) by A7,FUNCT_2:15
.= f.(G.(f".a,id I[01].b)) by A8,Lm4,FUNCT_3:def 8
.= f.(G.(f".a,b)) by FUNCT_1:18
.= f.((1-b)*f".a) by A1
.= ((1-b)*f".a)/.1 by A2
.= <*zz*>/.1 by A11
.= z by FINSEQ_4:16
.= (1-b)*a by A15,FINSEQ_1:76
.= F.(a,b) by A5
.= F.x by A7;
end;
f" is continuous by A3,TOPS_2:def 5;
then
A16: [:f",id I[01]:] is continuous;
G is continuous by A1,TOPALG_1:17;
hence thesis by A4,A16,A6,FUNCT_2:63;
end;
theorem Th7:
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
proof
deffunc Fa(Element of TOP-REAL 1, Element of I) = $2*$1;
consider G being Function of [:the carrier of TOP-REAL 1,I:], the carrier of
TOP-REAL 1 such that
A1: for x being Point of TOP-REAL 1, i being Point of I[01] holds G.(x,i
) = Fa(x,i) from BINOP_1:sch 4;
reconsider G as Function of [:TOP-REAL 1,I[01]:], TOP-REAL 1 by Lm2;
consider f being Function of TOP-REAL 1,R^1 such that
A2: for p being Element of TOP-REAL 1 holds f.p = p/.1 by JORDAN2B:1;
A3: f is being_homeomorphism by A2,JORDAN2B:28;
then
A4: f is continuous by TOPS_2:def 5;
let F be Function of [:R^1,I[01]:], R^1 such that
A5: for x being Point of R^1, i being Point of I[01] holds F.(x,i) = i*x;
A6: for x being Point of [:R^1,I[01]:] holds F.x = (f*(G*[:f",id I[01]:])).x
proof
reconsider ff = f as Function;
let x be Point of [:R^1,I[01]:];
consider a being Point of R^1, b being Point of I[01] such that
A7: x = [a,b] by BORSUK_1:10;
A8: dom (f") = the carrier of R^1 by FUNCT_2:def 1;
rng f = [#]R^1 by A3,TOPS_2:def 5;
then
A9: f is onto by FUNCT_2:def 3;
A10: dom f = the carrier of TOP-REAL 1 by FUNCT_2:def 1;
set g = ff";
consider z being Real such that
A11: b*f".a = <*z*> by JORDAN2B:20;
reconsider z as Element of REAL by XREAL_0:def 1;
A12: <*a*> = |[a]|;
then reconsider w = <*a*> as Element of REAL 1 by EUCLID:22;
A13: ff is one-to-one by A3,TOPS_2:def 5;
f.<*a*> = |[a]|/.1 by A2
.= a by Th4;
then <*a*> = g.a by A10,A13,A12,FUNCT_1:32;
then
A14: w = f/".a by A9,A13,TOPS_2:def 4;
A15: <*z*> = b*(f/".a) by A11
.= b*w by A14
.= <*b*a*> by RVSUM_1:47;
thus (f*(G*[:f",id I[01]:])).x = f.((G*[:f",id I[01]:]).x) by FUNCT_2:15
.= f.(G.([:f",id I[01]:].(a,b))) by A7,FUNCT_2:15
.= f.(G.(f".a,id I[01].b)) by A8,Lm4,FUNCT_3:def 8
.= f.(G.(f".a,b)) by FUNCT_1:18
.= f.(b*f".a) by A1
.= (b*f".a)/.1 by A2
.= <*z*>/.1 by A11
.= z by FINSEQ_4:16
.= b*a by A15,FINSEQ_1:76
.= F.(a,b) by A5
.= F.x by A7;
end;
f" is continuous by A3,TOPS_2:def 5;
then
A16: [:f",id I[01]:] is continuous;
G is continuous by A1,TOPALG_1:18;
hence thesis by A4,A16,A6,FUNCT_2:63;
end;
registration
cluster non empty interval for Subset of R^1;
existence
by TOPMETR:17;
end;
registration
let T be real-membered TopStruct;
cluster interval for Subset of T;
existence
proof
take {}T;
thus thesis;
end;
end;
definition
let T be real-membered TopStruct;
attr T is interval means
:Def3:
[#]T is interval;
end;
Lm7: for T being SubSpace of R^1 st T = R^1 holds T is interval
by TOPMETR:17;
registration
cluster strict non empty interval for SubSpace of R^1;
existence
proof
reconsider T = R^1 as strict non empty SubSpace of R^1 by TSEP_1:2;
take T;
thus thesis by Lm7;
end;
end;
definition
redefine func R^1 -> interval SubSpace of R^1; :: redefines R^1 (TOPMETR, definition)
coherence by Lm7,TSEP_1:2;
end;
theorem Th8:
for T being non empty interval SubSpace of R^1, a, b being Point
of T holds [. a, b .] c= the carrier of T
proof
let T be non empty interval SubSpace of R^1, a, b be Point of T;
reconsider a1 = a, b1 = b as Point of R^1 by PRE_TOPC:25;
[#]T is interval Subset of T by Def3;
then [. a1, b1 .] c= the carrier of T by XXREAL_2:def 12;
hence thesis;
end;
registration
cluster interval -> pathwise_connected for non empty SubSpace of R^1;
coherence
proof
let T be non empty SubSpace of R^1 such that
A1: T is interval;
let a, b be Point of T;
per cases;
suppose
A2: a <= b;
set f = L[01]((#)(a,b),(a,b)(#));
set X = Closed-Interval-TSpace(a,b);
A3: the carrier of X = [.a,b.] by A2,TOPMETR:18;
[.a,b.] c= the carrier of T by A1,Th8;
then reconsider f as Function of I[01], T by A3,FUNCT_2:7,TOPMETR:20;
take f;
the carrier of X is Subset of R^1 by TSEP_1:1;
then reconsider g = f as Function of I[01], R^1 by FUNCT_2:7,TOPMETR:20;
L[01]((#)(a,b),(a,b)(#)) is continuous by A2,TREAL_1:8;
then g is continuous by PRE_TOPC:26,TOPMETR:20;
hence f is continuous by PRE_TOPC:27;
thus f.0 = f.(#)(0,1) by TREAL_1:def 1
.= (#)(a,b) by A2,TREAL_1:9
.= a by A2,TREAL_1:def 1;
thus f.1 = f.(0,1)(#) by TREAL_1:def 2
.= (a,b)(#) by A2,TREAL_1:9
.= b by A2,TREAL_1:def 2;
end;
suppose
A4: b <= a;
set f = L[01]((b,a)(#),(#)(b,a));
set X = Closed-Interval-TSpace(b,a);
A5: the carrier of X = [.b,a.] by A4,TOPMETR:18;
[.b,a.] c= the carrier of T by A1,Th8;
then reconsider f as Function of I[01], T by A5,FUNCT_2:7,TOPMETR:20;
take f;
the carrier of X is Subset of R^1 by TSEP_1:1;
then reconsider g = f as Function of I[01], R^1 by FUNCT_2:7,TOPMETR:20;
L[01]((b,a)(#),(#)(b,a)) is continuous by A4,TREAL_1:8;
then g is continuous by PRE_TOPC:26,TOPMETR:20;
hence f is continuous by PRE_TOPC:27;
thus f.0 = f.(#)(0,1) by TREAL_1:def 1
.= (b,a)(#) by A4,TREAL_1:9
.= a by A4,TREAL_1:def 2;
thus f.1 = f.(0,1)(#) by TREAL_1:def 2
.= (#)(b,a) by A4,TREAL_1:9
.= b by A4,TREAL_1:def 1;
end;
end;
end;
theorem Th9:
a <= b implies Closed-Interval-TSpace(a,b) is interval
proof
set X = Closed-Interval-TSpace(a,b);
assume a <= b;
then [.a,b.] = [#]X by TOPMETR:18;
hence [#]X is interval;
end;
theorem Th10:
I[01] is interval by Th9,TOPMETR:20;
theorem
a <= b implies Closed-Interval-TSpace(a,b) is pathwise_connected
proof
assume a <= b;
then reconsider
X = Closed-Interval-TSpace(a,b) as non empty interval SubSpace of
R^1 by Th9;
X is pathwise_connected;
hence thesis;
end;
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
:Def4:
for s, t being Element of I[01] holds it.(s,t) = (1-t) * P.s + t * Q.s;
existence
proof
defpred P[Element of I, Element of I, set] means $3 = (1-$2) * P.$1 + $2 *
Q.$1;
A1: for m, n being Element of I ex z being Element of T st P[m,n,z]
proof
let m, n be Element of I;
A2: 0 <= n by BORSUK_1:43;
set z = (1-n) * P.m + n * Q.m;
A3: n <= 1 by BORSUK_1:43;
per cases;
suppose
P.m <= Q.m;
then P.m <= z & z <= Q.m by A2,A3,XREAL_1:172,173;
then
A4: z in [. P.m,Q.m .] by XXREAL_1:1;
[. P.m,Q.m .] c= the carrier of T by Th8;
hence thesis by A4;
end;
suppose
A5: P.m > Q.m;
1-1 <= 1-n by A3,XREAL_1:13;
then (1-n)*Q.m <= (1-n)*P.m by A5,XREAL_1:64;
then
A6: (1-n)*Q.m+n*Q.m <= (1-n)*P.m+n*Q.m by XREAL_1:6;
A7: [. Q.m, P.m .] c= the carrier of T by Th8;
Q.m - P.m < Q.m - Q.m by A5,XREAL_1:15;
then n*(Q.m-P.m) <= n*0 by A2,XREAL_1:131;
then P.m+n*(Q.m-P.m) <= P.m+0 by XREAL_1:6;
then z in [. Q.m, P.m .] by A6,XXREAL_1:1;
hence thesis by A7;
end;
end;
consider F being Function of [:I,I:], the carrier of T such that
A8: for m, n being Element of I holds P[m,n,F.(m,n)] from BINOP_1:sch
3(A1 );
reconsider F as Function of [:I[01],I[01]:], T by Lm1;
take F;
let s, t be Element of I;
thus thesis by A8;
end;
uniqueness
proof
let f, g be Function of [:I[01],I[01]:], T such that
A9: for s, t being Element of I[01] holds f.(s,t) = (1-t) * P.s + t * Q.s and
A10: for s, t being Element of I[01] holds g.(s,t) = (1-t) * P.s + t * Q.s;
for s, t being Element of I holds f.(s,t) = g.(s,t)
proof
let s, t be Element of I;
thus f.(s,t) = (1-t) * P.s + t * Q.s by A9
.= g.(s,t) by A10;
end;
hence f = g by Lm1,BINOP_1:2;
end;
end;
Lm8: for T being non empty interval SubSpace of R^1, P, Q being continuous
Function of I[01],T holds R1Homotopy(P,Q) is continuous
proof
set E = the carrier of R^1;
let T be non empty interval SubSpace of R^1, P, Q be continuous Function of
I[01],T;
set F = R1Homotopy(P,Q);
set PI = [:P,id I[01]:];
set QI = [:Q,id I[01]:];
defpred Fa[Element of E,Element of I,set] means $3 = (1-$2)*$1;
defpred Fb[Element of E,Element of I,set] means $3 = $2*$1;
A1: the carrier of T is Subset of R^1 by TSEP_1:1;
then reconsider G = F as Function of [:I[01],I[01]:],R^1 by FUNCT_2:7;
reconsider P1 = P, Q1 = Q as Function of I[01],R^1 by A1,FUNCT_2:7;
reconsider P1, Q1 as continuous Function of I[01],R^1 by PRE_TOPC:26;
set P1I = [:P1,id I[01]:];
set Q1I = [:Q1,id I[01]:];
A2: for x being Element of E for y being Element of I ex z being Element of
E st Fa[x,y,z]
proof let x be Element of E;
let y be Element of I;
(1-y)*x in REAL by XREAL_0:def 1;
then reconsider z = (1-y)*x as Element of E by TOPMETR:17;
take z;
thus thesis;
end;
consider Pa being Function of [:E,I:],E such that
A3: for x being Element of E, i being Element of I holds Fa[x,i,Pa.(x,i)
] from BINOP_1:sch 3(A2);
A4: for x being Element of E for y being Element of I ex z being Element of
E st Fb[x,y,z]
proof
let x be Element of E, y be Element of I;
y*x in REAL by XREAL_0:def 1;
hence thesis by TOPMETR:17;
end;
consider Pb being Function of [:E,I:],E such that
A5: for x being Element of E, i being Element of I holds Fb[x,i, Pb.(x,i
)] from BINOP_1:sch 3(A4);
reconsider Pa, Pb as Function of [:R^1,I[01]:],R^1 by Lm3;
A6: Pb is continuous by A5,Th7;
Pa is continuous by A3,Th6;
then consider g being Function of [:I[01],I[01]:],R^1 such that
A7: for p being Point of [:I[01],I[01]:],r1,r2 being Real st (Pa
*P1I).p=r1 & (Pb*Q1I).p=r2 holds g.p=r1+r2 and
A8: g is continuous by A6,JGRAPH_2:19;
A9: for p being Point of [:I[01],I[01]:] holds G.p = (Pa*P1I).p + (Pb*Q1I). p
proof
A10: dom Q = I by FUNCT_2:def 1;
A11: dom P = I by FUNCT_2:def 1;
let p be Point of [:I[01],I[01]:];
consider s, t being Point of I[01] such that
A12: p = [s,t] by BORSUK_1:10;
reconsider a1 = P.s, b1 = Q.s as Point of R^1 by PRE_TOPC:25;
A13: P.s in the carrier of T;
A14: F.(s,t) = (1-t) * a1 + t * b1 by Def4;
A15: Q.s in the carrier of T;
A16: (id I[01]).t = t by FUNCT_1:18;
A17: (Pb*QI).p = Pb.(QI.(s,t)) by A12,FUNCT_2:15
.= Pb.(Q.s,t) by A10,A16,Lm4,FUNCT_3:def 8
.= t * Q.s by A1,A5,A15;
(Pa*PI).p = Pa.(PI.(s,t)) by A12,FUNCT_2:15
.= Pa.(P.s,t) by A11,A16,Lm4,FUNCT_3:def 8
.= (1-t) * P.s by A1,A3,A13;
hence thesis by A12,A17,A14;
end;
for p being Point of [:I[01],I[01]:] holds G.p = g.p
proof
let p be Point of [:I[01],I[01]:];
thus G.p = (Pa*P1I).p + (Pb*Q1I).p by A9
.= g.p by A7;
end;
hence thesis by A8,FUNCT_2:63,PRE_TOPC:27;
end;
Lm9: for T being non empty interval SubSpace of R^1, a, b being Point of T,
P, Q
being Path of a,b holds for s being Point of I[01] holds R1Homotopy(P,Q).(s,0)
= P.s & R1Homotopy(P,Q).(s,1) = Q.s & for t being Point of I[01] holds
R1Homotopy(P,Q).(0,t) = a & R1Homotopy(P,Q).(1,t) = b
proof
let T be non empty interval SubSpace of R^1, a, b be Point of T, P, Q be Path
of a,b;
set F = R1Homotopy(P,Q);
let s be Point of I[01];
A1: P.0[01] = a & Q.0[01] = a by BORSUK_2:def 4;
thus F.(s,0) = (1-0) * P.s + 0 * Q.s by Def4,BORSUK_1:def 14
.= P.s;
thus F.(s,1) = (1-1) * P.s + 1 * Q.s by Def4,BORSUK_1:def 15
.= Q.s;
let t be Point of I[01];
thus F.(0,t) = (1-t) * P.0[01] + t * Q.0[01] by Def4
.= a by A1;
A2: P.1[01] = b & Q.1[01] = b by BORSUK_2:def 4;
thus F.(1,t) = (1-t) * P.1[01] + t * Q.1[01] by Def4
.= b by A2;
end;
theorem Th12:
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
proof
let T be non empty interval SubSpace of R^1, a, b be Point of T, P, Q be Path
of a,b;
take F = R1Homotopy(P,Q);
thus F is continuous by Lm8;
thus thesis by Lm9;
end;
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;
coherence
proof
let F be Homotopy of P,Q;
P, Q are_homotopic by Th12;
hence thesis by BORSUK_6:def 11;
end;
end;
theorem Th13:
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) }
proof
let T be non empty interval SubSpace of R^1, a be Point of T, C be Loop of a;
set E = EqRel(T,a);
hereby
let x be object;
assume x in the carrier of pi_1(T,a);
then consider P being Loop of a such that
A1: x = Class(E,P) by TOPALG_1:47;
P,C are_homotopic by Th12;
then x = Class(E,C) by A1,TOPALG_1:46;
hence x in { Class(E,C) } by TARSKI:def 1;
end;
let x be object;
assume x in { Class(E,C) };
then
A2: x = Class(E,C) by TARSKI:def 1;
C in Loops a by TOPALG_1:def 1;
then x in Class E by A2,EQREL_1:def 3;
hence thesis by TOPALG_1:def 5;
end;
registration
let T be non empty interval SubSpace of R^1, a be Point of T;
cluster pi_1(T,a) -> trivial;
coherence
proof
set C = the constant Loop of a;
set E = EqRel(T,a);
the carrier of pi_1(T,a) = Class E by TOPALG_1:def 5;
then { Class(E,C) } = Class E by Th13;
hence thesis by TOPALG_1:def 5;
end;
end;
theorem
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
proof
assume
A1: a <= b;
let x, y be Point of Closed-Interval-TSpace(a,b), P, Q be Path of x,y;
Closed-Interval-TSpace(a,b) is interval by A1,Th9;
hence thesis by Th12;
end;
theorem
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) }
proof
assume
A1: a <= b;
let x be Point of Closed-Interval-TSpace(a,b), C be Loop of x;
Closed-Interval-TSpace(a,b) is interval by A1,Th9;
hence thesis by Th13;
end;
theorem
for x, y being Point of I[01], P, Q being Path of x,y holds P, Q
are_homotopic by Th10,Th12;
theorem
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) } by Th10,Th13;
registration
let x be Point of I[01];
cluster pi_1(I[01],x) -> trivial;
coherence by Th10;
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;
coherence by Lm5;
end;
theorem
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
proof
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;
thus P, Q are_homotopic by Th2;
thus ConvexHomotopy(P,Q) is continuous;
thus thesis by Lm6;
end;
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;
coherence by Lm8;
end;
theorem
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
proof
let T be non empty interval SubSpace of R^1, a, b be Point of T, P, Q be Path
of a,b;
thus P, Q are_homotopic by Th12;
thus R1Homotopy(P,Q) is continuous;
thus thesis by Lm9;
end;