:: The Fundamental Group
:: by Artur Korni{\l}owicz , Yasunari Shidama and Adam Grabowski
::
:: Received March 18, 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, NAT_1, GROUP_1, GROUP_6, RELAT_1, FUNCT_2, STRUCT_0,
FUNCT_1, SUBSET_1, BORSUK_1, PRE_TOPC, XXREAL_1, CARD_1, XBOOLE_0,
XXREAL_0, REAL_1, ARYTM_3, RCOMP_1, TARSKI, VALUED_0, FINSEQ_1, ARYTM_1,
COMPLEX1, EUCLID, METRIC_1, FINSEQ_2, ORDINAL2, TOPS_1, SUPINF_2,
ZFMISC_1, BORSUK_2, GRAPH_1, ALGSTR_1, EQREL_1, WAYBEL20, PARTFUN1,
RELAT_2, ALGSTR_0, BINOP_1, WELLORD1, BORSUK_6, TOPALG_1, MSSUBFAM;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, EQREL_1, FUNCT_1, RELSET_1,
PARTFUN1, FUNCT_2, RELAT_2, BINOP_1, ORDINAL1, NUMBERS, XCMPLX_0,
XXREAL_0, XREAL_0, COMPLEX1, REAL_1, RCOMP_1, FINSEQ_1, VALUED_0,
RVSUM_1, FINSEQ_2, STRUCT_0, ALGSTR_0, METRIC_1, PRE_TOPC, TOPS_1,
TOPS_2, GROUP_1, BORSUK_1, RLVECT_1, EUCLID, BORSUK_2, GROUP_6, BORSUK_6;
constructors BINOP_2, COMPLEX1, REAL_1, RCOMP_1, TOPS_1, TOPS_2, GROUP_6,
T_0TOPSP, EUCLID, BORSUK_6, MONOID_0, BINOP_1;
registrations RELSET_1, FUNCT_2, XXREAL_0, XREAL_0, MEMBERED, EQREL_1,
STRUCT_0, TOPS_1, BORSUK_1, EUCLID, BORSUK_2, JORDAN5A, VALUED_0,
ZFMISC_1, MONOID_0, PRE_TOPC, RVSUM_1, TOPMETR, ORDINAL1;
requirements BOOLE, SUBSET, NUMERALS, ARITHM, REAL;
definitions TARSKI, XBOOLE_0, RELAT_1, FUNCT_1, FUNCT_2, STRUCT_0, GROUP_1,
BORSUK_2, GROUP_6, BORSUK_6;
equalities XBOOLE_0, STRUCT_0, BINOP_1, BORSUK_1, ALGSTR_0, VALUED_1;
expansions TARSKI, FUNCT_1, FUNCT_2;
theorems BORSUK_2, ZFMISC_1, EQREL_1, BINOP_1, FUNCT_2, RELAT_1, TARSKI,
BORSUK_1, TOPS_2, EUCLID, XBOOLE_0, TOPS_1, BORSUK_6, JORDAN5B, JGRAPH_2,
XBOOLE_1, XCMPLX_1, FUNCT_1, TOPREAL3, GOBOARD6, METRIC_1, SPPOL_1,
RVSUM_1, ABSVALUE, RCOMP_1, FUNCT_3, GROUP_1, UNIFORM1, BORSUK_4,
SUBSET_1, GROUP_6, XREAL_1, JGRAPH_6, COMPLEX1, XXREAL_0, XXREAL_1,
RLVECT_1, RFUNCT_1, VALUED_1, RLVECT_4;
schemes EQREL_1, BINOP_1, XBOOLE_0, FUNCT_2;
begin :: Preliminaries
reserve p, q, x, y for Real,
n for Nat;
theorem
for G, H being set, g being Function of G,H, h being Function of H,G
st h * g = id G & g * h = id H holds h is bijective
by FUNCT_2:23;
theorem Th2:
for X being Subset of I[01], a being Point of I[01] st X = ]. a, 1 .]
holds X` = [. 0, a .]
proof
set I = the carrier of I[01];
let X be Subset of I[01], a be Point of I[01] such that
A1: X = ]. a, 1 .];
set Y = [. 0,a .];
A2: X` = I \ X by SUBSET_1:def 4;
hereby
let x be object;
assume
A3: x in X`;
then reconsider y = x as Point of I[01];
not x in X by A2,A3,XBOOLE_0:def 5;
then
A4: y <= a or y > 1 by A1,XXREAL_1:2;
0 <= y by BORSUK_1:43;
hence x in Y by A4,BORSUK_1:43,XXREAL_1:1;
end;
let x be object;
assume
A5: x in Y;
then reconsider y = x as Real;
A6: 0 <= y by A5,XXREAL_1:1;
A7: y <= a by A5,XXREAL_1:1;
a <= 1 by BORSUK_1:43;
then y <= 1 by A7,XXREAL_0:2;
then
A8: y in I by A6,BORSUK_1:43;
not y in X by A1,A7,XXREAL_1:2;
hence thesis by A2,A8,XBOOLE_0:def 5;
end;
theorem Th3:
for X being Subset of I[01], a being Point of I[01] st X = [. 0, a .[
holds X` = [. a, 1 .]
proof
set I = the carrier of I[01];
let X be Subset of I[01], a be Point of I[01] such that
A1: X = [. 0, a .[;
set Y = [. a,1 .];
A2: X` = I \ X by SUBSET_1:def 4;
hereby
let x be object;
assume
A3: x in X`;
then reconsider y = x as Point of I[01];
not x in X by A2,A3,XBOOLE_0:def 5;
then
A4: y >= a or y < 0 by A1,XXREAL_1:3;
y <= 1 by BORSUK_1:43;
hence x in Y by A4,BORSUK_1:43,XXREAL_1:1;
end;
let x be object;
assume
A5: x in Y;
then reconsider y = x as Real;
A6: a <= y by A5,XXREAL_1:1;
then
A7: not y in X by A1,XXREAL_1:3;
A8: 0 <= a by BORSUK_1:43;
y <= 1 by A5,XXREAL_1:1;
then y in I by A6,A8,BORSUK_1:43;
hence thesis by A2,A7,XBOOLE_0:def 5;
end;
theorem Th4:
for X being Subset of I[01], a being Point of I[01] st X = ]. a, 1 .]
holds X is open
proof
let X be Subset of I[01], a be Point of I[01] such that
A1: X = ]. a, 1 .];
set Y = [. 0,a .];
Y c= the carrier of I[01]
proof
let x be object;
A2: a <= 1 by BORSUK_1:43;
assume
A3: x in Y;
then reconsider x as Real;
A4: 0 <= x by A3,XXREAL_1:1;
x <= a by A3,XXREAL_1:1;
then x <= 1 by A2,XXREAL_0:2;
hence thesis by A4,BORSUK_1:43;
end;
then reconsider Y as Subset of I[01];
Y is closed & X` = Y by A1,Th2,BORSUK_4:23;
hence thesis by TOPS_1:4;
end;
theorem Th5:
for X being Subset of I[01], a being Point of I[01] st X = [. 0, a .[
holds X is open
proof
let X be Subset of I[01], a be Point of I[01] such that
A1: X = [. 0, a .[;
set Y = [. a,1 .];
Y c= the carrier of I[01]
proof
let x be object;
A2: 0 <= a by BORSUK_1:43;
assume
A3: x in Y;
then reconsider x as Real;
x <= 1 & a <= x by A3,XXREAL_1:1;
hence thesis by A2,BORSUK_1:43;
end;
then reconsider Y as Subset of I[01];
Y is closed & X` = Y by A1,Th3,BORSUK_4:23;
hence thesis by TOPS_1:4;
end;
theorem
for f being real-valued FinSequence holds x * (-f) = - (x*f)
proof
let f be real-valued FinSequence;
thus x * (-f) = x*((-1)*f) .= (-1) * x*f by RVSUM_1:49
.= - x*f by RVSUM_1:49;
end;
theorem Th7:
for f, g being real-valued FinSequence holds x * (f-g) = x*f - x*g
by RFUNCT_1:18;
theorem Th8:
for f being real-valued FinSequence holds (x-y) * f = x*f - y*f
proof
let f be real-valued FinSequence;
A1: dom ((x-y)*f) = dom f by VALUED_1:def 5;
A2: dom (x*f-y*f) = dom(x*f) /\ dom(y*f) by VALUED_1:12;
A3: dom (x*f) = dom f by VALUED_1:def 5;
A4: dom (y*f) = dom f by VALUED_1:def 5;
now
let n;
assume
A5: n in dom ((x-y)*f);
thus ((x-y) * f).n = (x-y)*(f.n) by VALUED_1:6
.= x*(f.n)-y*(f.n)
.= x*f.n-(y*f).n by VALUED_1:6
.= (x*f).n-(y*f).n by VALUED_1:6
.= (x*f - y*f).n by A1,A2,A3,A4,A5,VALUED_1:13;
end;
hence thesis by A1,A2,A3,A4;
end;
theorem Th9:
for f, g, h, k being real-valued FinSequence holds (f+g)-(h+k) = (f-h)+(g-k)
proof
let f, g, h, k be real-valued FinSequence;
thus f+g-(h+k) = f+(g+-(h+k)) by RVSUM_1:15
.= f+(g+(-h+-k)) by RVSUM_1:26
.= f+(-h+(g+-k)) by RVSUM_1:15
.= f+-h+(g+-k) by RVSUM_1:15
.= (f-h)+(g+-k)
.= (f-h) + (g-k);
end;
theorem Th10:
for f being Element of REAL n st 0 <= x & x <= 1 holds |.x*f.| <= |.f.|
proof
let f be Element of REAL n such that
A1: 0 <= x and
A2: x <= 1;
|.x*f.| = |.x.|*|.f.| & x = |.x.| by A1,ABSVALUE:def 1,EUCLID:11;
then |.x*f.| <= 1*|.f.| by A1,A2,XREAL_1:66;
hence thesis;
end;
theorem
for f being Element of REAL n, p being Point of I[01] holds |.p*f.| <= |.f.|
proof
let f be Element of REAL n, p be Point of I[01];
[. 0,1 .] = {r where r is Real: 0 <= r & r <= 1 } &
p in the carrier of I[01] by RCOMP_1:def 1;
then ex r being Real st r = p & 0 <= r & r <= 1 by BORSUK_1:40;
hence thesis by Th10;
end;
theorem
for e1, e2, e3, e4, e5, e6 being Point of Euclid n, p1, p2, p3, p4
being Point of TOP-REAL n st e1 = p1 & e2 = p2 & e3 = p3 & e4 = p4 & e5 = p1+p3
& e6 = p2+p4 & dist(e1,e2) < x & dist(e3,e4) < y holds dist(e5,e6) < x+y
proof
let e1, e2, e3, e4, e5, e6 be Point of Euclid n, p1, p2, p3, p4 be Point of
TOP-REAL n such that
A1: e1 = p1 and
A2: e2 = p2 and
A3: e3 = p3 and
A4: e4 = p4 and
A5: e5 = p1+p3 and
A6: e6 = p2+p4 and
A7: dist(e1,e2) < x & dist(e3,e4) < y;
reconsider f1 = e1, f2 = e2, f3 = e3, f4 = e4, f5=e5, f6 = e6 as Element of
REAL n by A1,A2,A3,A4,A5,A6,EUCLID:22;
A8: |. f1-f2 + (f3-f4) .| <= |. f1-f2 .| + |. f3-f4 .| & dist(e1,e2) + dist
(e3, e4) < x + y by A7,EUCLID:12,XREAL_1:8;
reconsider u1 = f1, u2 = f2, u3 = f3, u4 = f4, u6 = f6 as Element of n
-tuples_on REAL by EUCLID:def 1;
u2+u4 = u6 by A2,A4,A6;
then
A9: f1+f3-f6 = (u1-u2)+(u3-u4) by Th9
.= (f1-f2) + (f3-f4);
A10: dist(e1,e2) = |. f1-f2 .| & dist(e3,e4) = |. f3-f4 .| by SPPOL_1:5;
dist(e5,e6) = |.f5-f6.| by SPPOL_1:5
.= |. (f1-f2) + (f3-f4) .| by A1,A3,A5,A9;
hence thesis by A10,A8,XXREAL_0:2;
end;
theorem Th13:
for e1, e2, e5, e6 being Point of Euclid n, p1, p2 being Point
of TOP-REAL n st e1 = p1 & e2 = p2 & e5 = y*p1 & e6 = y*p2 & dist(e1,e2) < x &
y <> 0 holds dist(e5,e6) < |.y.|*x
proof
let e1, e2, e5, e6 be Point of Euclid n, p1, p2 be Point of TOP-REAL n such
that
A1: e1 = p1 and
A2: e2 = p2 and
A3: e5 = y*p1 and
A4: e6 = y*p2 and
A5: dist(e1,e2) < x and
A6: y <> 0;
reconsider f1 = e1, f2 = e2, f5= e5, f6 = e6 as Element of REAL n by A1,A2,A3
,A4,EUCLID:22;
A7: dist(e1,e2) = |. f1-f2 .| by SPPOL_1:5;
A8: 0 < |.y.| by A6,COMPLEX1:47;
dist(e5,e6) = |.f5-f6.| by SPPOL_1:5
.= |. y*f1-f6 .| by A1,A3
.= |. y*f1-y*f2 .| by A2,A4
.= |. y*(f1-f2) .| by Th7
.= |.y.| * |. f1-f2 .| by EUCLID:11;
hence thesis by A5,A7,A8,XREAL_1:68;
end;
theorem Th14:
for e1, e2, e3, e4, e5, e6 being Point of Euclid n, p1, p2, p3,
p4 being Point of TOP-REAL n st e1 = p1 & e2 = p2 & e3 = p3 & e4 = p4 & e5 = x*
p1+y*p3 & e6 = x*p2+y*p4 & dist(e1,e2) < p & dist(e3,e4) < q & x <> 0 & y <> 0
holds dist(e5,e6) < |.x.|*p + |.y.|*q
proof
let e1, e2, e3, e4, e5, e6 be Point of Euclid n, p1, p2, p3, p4 be Point of
TOP-REAL n such that
A1: e1 = p1 and
A2: e2 = p2 and
A3: e3 = p3 and
A4: e4 = p4 and
A5: e5 = x*p1+y*p3 and
A6: e6 = x*p2+y*p4 and
A7: dist(e1,e2) < p and
A8: dist(e3,e4) < q and
A9: x <> 0 and
A10: y <> 0;
reconsider f1 = e1, f2 = e2, f3 = e3, f4 = e4, f5 = e5, f6 = e6 as Element
of REAL n by A1,A2,A3,A4,A5,A6,EUCLID:22;
A11: x*f2 = x*p2 & y*f4 = y*p4 by A2,A4;
x*f1 = x*p1 & y*f3 = y*p3 by A1,A3;
then
A12: f5 = x*f1+y*f3 by A5;
A13: 0 < |.y.| by A10,COMPLEX1:47;
dist(e3,e4) = |. f3-f4 .| by SPPOL_1:5;
then
A14: |.y.|*|.f3-f4.| < |.y.|*q by A8,A13,XREAL_1:68;
A15: 0 < |.x.| by A9,COMPLEX1:47;
dist(e1,e2) = |. f1-f2 .| by SPPOL_1:5;
then |.x.|*|.f1-f2.| < |.x.|*p by A7,A15,XREAL_1:68;
then
A16: |.x.|*|.f1-f2.| + |.y.|*|.f3-f4.| < |.x.|*p + |.y.|*q by A14,XREAL_1:8;
|. x*(f1-f2) + y*(f3-f4) .| <= |. x*(f1-f2) .| + |. y*(f3-f4) .| by EUCLID:12
;
then |. x*(f1-f2) + y*(f3-f4) .| <= |.x*(f1-f2).| + |.y.|*|.(f3-f4).| by
EUCLID:11;
then
A17: |. x*(f1-f2) + y*(f3-f4) .| <= |.x.|*|.f1-f2.| + |.y.|*|.f3-f4 .| by
EUCLID:11;
dist(e5,e6) = |.f5-f6.| by SPPOL_1:5
.= |. x*f1+y*f3 - (x*f2+y*f4) .| by A6,A12,A11
.= |. (x*f1-x*f2) + (y*f3-y*f4) .| by Th9
.= |. x*(f1-f2) + (y*f3-y*f4) .| by Th7
.= |. x*(f1-f2) + y*(f3-f4) .| by Th7;
hence thesis by A17,A16,XXREAL_0:2;
end;
Lm1: for X being non empty TopSpace, f1, f2, g being Function of X,TOP-REAL n
st f1 is continuous & f2 is continuous & for p being Point of X holds g.p = f1.
p + f2.p holds g is continuous
proof
let X being non empty TopSpace, f1, f2, g be Function of X,TOP-REAL n such
that
A1: f1 is continuous & f2 is continuous and
A2: for p being Point of X holds g.p = f1.p + f2.p;
consider h being Function of X,TOP-REAL n such that
A3: for r being Point of X holds h.r = f1.r + f2.r and
A4: h is continuous by A1,JGRAPH_6:12;
for x being Point of X holds g.x = h.x
proof
let x be Point of X;
thus g.x = f1.x + f2.x by A2
.= h.x by A3;
end;
hence thesis by A4,FUNCT_2:63;
end;
theorem Th15:
for X being non empty TopSpace, f, g being Function of X,
TOP-REAL n st f is continuous & for p being Point of X holds g.p = y * f.p
holds g is continuous
proof
let X being non empty TopSpace, f, g be Function of X,TOP-REAL n such that
A1: f is continuous and
A2: for p being Point of X holds g.p = y * f.p;
for p being Point of X, V being Subset of TOP-REAL n st g.p in V & V is
open ex W being Subset of X st p in W & W is open & g.:W c= V
proof
let p be Point of X, V be Subset of TOP-REAL n;
reconsider r = g.p as Point of Euclid n by TOPREAL3:8;
reconsider r1 = f.p as Point of Euclid n by TOPREAL3:8;
assume g.p in V & V is open;
then g.p in Int V by TOPS_1:23;
then consider r0 being Real such that
A3: r0 > 0 and
A4: Ball(r,r0) c= V by GOBOARD6:5;
reconsider G1 = Ball(r1,r0/|.y.|) as Subset of TOP-REAL n by TOPREAL3:8;
per cases;
suppose
A5: y <> 0;
A6: G1 is open by GOBOARD6:3;
A7: 0 < |.y.| by A5,COMPLEX1:47;
then r1 in G1 by A3,GOBOARD6:1,XREAL_1:139;
then consider W1 being Subset of X such that
A8: p in W1 and
A9: W1 is open and
A10: f.:W1 c= G1 by A1,A6,JGRAPH_2:10;
take W1;
thus p in W1 by A8;
thus W1 is open by A9;
g.:W1 c= Ball(r,r0)
proof
let x be object;
assume x in g.:W1;
then consider z being object such that
A11: z in dom g and
A12: z in W1 and
A13: g.z = x by FUNCT_1:def 6;
reconsider z as Point of X by A11;
A14: x = y * f.z by A2,A13;
then reconsider e1x = x as Point of Euclid n by TOPREAL3:8;
reconsider ea1 = f.z as Point of Euclid n by TOPREAL3:8;
z in the carrier of X;
then z in dom f by FUNCT_2:def 1;
then f.z in f.:W1 by A12,FUNCT_1:def 6;
then
A15: dist(r1,ea1) < r0/|.y.| by A10,METRIC_1:11;
r = y * f.p by A2;
then dist(r,e1x) < |.y.|*(r0/|.y.|) by A5,A14,A15,Th13;
then dist(r,e1x) < r0 by A7,XCMPLX_1:87;
hence thesis by METRIC_1:11;
end;
hence thesis by A4;
end;
suppose
A16: y = 0;
A17: r = y * f.p by A2
.= 0.TOP-REAL n by A16,RLVECT_1:10;
take W = [#]X;
thus p in W;
thus W is open;
let x be object;
assume x in g.:W;
then consider z being object such that
z in dom g and
A18: z in W and
A19: g.z = x by FUNCT_1:def 6;
reconsider z as Point of X by A18;
x = y * f.z by A2,A19
.= 0.TOP-REAL n by A16,RLVECT_1:10;
then x in Ball(r,r0) by A3,A17,GOBOARD6:1;
hence thesis by A4;
end;
end;
hence thesis by JGRAPH_2:10;
end;
theorem
for X being non empty TopSpace, f1, f2, g being Function of X,TOP-REAL
n st f1 is continuous & f2 is continuous & for p being Point of X holds g.p = x
* f1.p + y * f2.p holds g is continuous
proof
let X being non empty TopSpace, f1, f2, g be Function of X,TOP-REAL n such
that
A1: f1 is continuous and
A2: f2 is continuous and
A3: for p being Point of X holds g.p = x*f1.p + y*f2.p;
per cases;
suppose that
A4: x <> 0 and
A5: y <> 0;
for p being Point of X, V being Subset of TOP-REAL n st g.p in V & V
is open ex W being Subset of X st p in W & W is open & g.:W c= V
proof
let p be Point of X, V be Subset of TOP-REAL n;
reconsider r = g.p as Point of Euclid n by TOPREAL3:8;
assume g.p in V & V is open;
then g.p in Int V by TOPS_1:23;
then consider r0 being Real such that
A6: r0 > 0 and
A7: Ball(r,r0) c= V by GOBOARD6:5;
A8: r0/2 > 0 by A6,XREAL_1:215;
reconsider r2 = f2.p as Point of Euclid n by TOPREAL3:8;
reconsider G2 = Ball(r2,r0/2/|.y.|) as Subset of TOP-REAL n by TOPREAL3:8
;
A9: G2 is open by GOBOARD6:3;
reconsider r1 = f1.p as Point of Euclid n by TOPREAL3:8;
reconsider G1 = Ball(r1,r0/2/|.x.|) as Subset of TOP-REAL n by TOPREAL3:8
;
A10: G1 is open by GOBOARD6:3;
A11: |.y.| > 0 by A5,COMPLEX1:47;
then r2 in G2 by A8,GOBOARD6:1,XREAL_1:139;
then consider W2 being Subset of X such that
A12: p in W2 and
A13: W2 is open and
A14: f2.:W2 c= G2 by A2,A9,JGRAPH_2:10;
A15: |.x.| > 0 by A4,COMPLEX1:47;
then r1 in G1 by A8,GOBOARD6:1,XREAL_1:139;
then consider W1 being Subset of X such that
A16: p in W1 and
A17: W1 is open and
A18: f1.:W1 c= G1 by A1,A10,JGRAPH_2:10;
take W = W1 /\ W2;
thus p in W by A16,A12,XBOOLE_0:def 4;
thus W is open by A17,A13;
g.:W c= Ball(r,r0)
proof
let a be object;
assume a in g.:W;
then consider z being object such that
A19: z in dom g and
A20: z in W and
A21: g.z = a by FUNCT_1:def 6;
A22: z in W1 by A20,XBOOLE_0:def 4;
reconsider z as Point of X by A19;
reconsider ea2 = f2.z as Point of Euclid n by TOPREAL3:8;
reconsider ea1 = f1.z as Point of Euclid n by TOPREAL3:8;
A23: z in the carrier of X;
then
A24: z in dom f2 by FUNCT_2:def 1;
z in W2 by A20,XBOOLE_0:def 4;
then f2.z in f2.:W2 by A24,FUNCT_1:def 6;
then
A25: dist(r2,ea2) < r0/2/|.y.| by A14,METRIC_1:11;
z in dom f1 by A23,FUNCT_2:def 1;
then f1.z in f1.:W1 by A22,FUNCT_1:def 6;
then
A26: dist(r1,ea1) < r0/2/|.x.| by A18,METRIC_1:11;
A27: a = x*f1.z + y*f2.z by A3,A21;
then reconsider e1x = a as Point of Euclid n by TOPREAL3:8;
r = x*f1.p + y*f2.p by A3;
then dist(r,e1x) < |.x.|*(r0/2/|.x.|) + |.y.|*(r0/2/|.y.|) by A4,A5,A27
,A26,A25,Th14;
then dist(r,e1x) < |.x.|*(r0/|.x.|/2) + |.y.|*(r0/2/|.y.|) by
XCMPLX_1:48;
then dist(r,e1x) < |.x.|*(r0/|.x.|/2) + |.y.|*(r0/|.y.|/2) by
XCMPLX_1:48;
then dist(r,e1x) < r0/2 + |.y.|*(r0/|.y.|/2) by A15,XCMPLX_1:97;
then dist(r,e1x) < r0/2 + r0/2 by A11,XCMPLX_1:97;
hence thesis by METRIC_1:11;
end;
hence thesis by A7;
end;
hence thesis by JGRAPH_2:10;
end;
suppose
A28: x = 0;
for p being Point of X holds g.p = y * f2.p
proof
let p be Point of X;
thus g.p = x*f1.p + y*f2.p by A3
.= 0.TOP-REAL n + y*f2.p by A28,RLVECT_1:10
.= y*f2.p by RLVECT_1:4;
end;
hence thesis by A2,Th15;
end;
suppose
A29: y = 0;
for p being Point of X holds g.p = x * f1.p
proof
let p be Point of X;
thus g.p = x*f1.p + y*f2.p by A3
.= x*f1.p + 0.TOP-REAL n by A29,RLVECT_1:10
.= x*f1.p by RLVECT_1:4;
end;
hence thesis by A1,Th15;
end;
end;
theorem Th17:
for F being Function of [:TOP-REAL n,I[01]:], TOP-REAL n st for
x being Point of TOP-REAL n, i being Point of I[01] holds F.(x,i) = (1-i) * x
holds F is continuous
proof
set I = the carrier of I[01];
let F be Function of [:TOP-REAL n,I[01]:], TOP-REAL n such that
A1: for x being Point of TOP-REAL n, i being Point of I[01] holds F.(x,i
) = (1-i) * x;
A2: REAL n = n-tuples_on REAL by EUCLID:def 1;
A3: [#]I[01] = I;
for p being Point of [:TOP-REAL n,I[01]:], V being Subset of TOP-REAL n
st F.p in V & V is open ex W being Subset of [:TOP-REAL n,I[01]:] st p in W & W
is open & F.:W c= V
proof
let p be Point of [:TOP-REAL n,I[01]:], V be Subset of TOP-REAL n;
reconsider ep = F.p as Point of Euclid n by TOPREAL3:8;
consider x being Point of TOP-REAL n, i being Point of I[01] such that
A4: p = [x,i] by BORSUK_1:10;
A5: ep = F.(x,i) by A4
.= (1-i)*x by A1;
reconsider fx = x as Element of REAL n by EUCLID:22;
reconsider lx = x as Point of Euclid n by TOPREAL3:8;
assume F.p in V & V is open;
then F.p in Int V by TOPS_1:23;
then consider r0 being Real such that
A6: r0 > 0 and
A7: Ball(ep,r0) c= V by GOBOARD6:5;
A8: r0/2 > 0 by A6,XREAL_1:139;
per cases;
suppose
A9: 1-i > 0;
then --(1-i) > -0;
then -(1-i) < 0;
then
A10: (i-1)*(2*(1-i)*|.fx.|) <= 0 by A9;
set t = 2*(1-i)*|.fx.|+r0;
set c = (1-i)*r0 / t;
i+c = i*t/t + ((1-i)*r0 / t) by A6,A9,XCMPLX_1:89
.= (i*t + (1-i)*r0) / t by XCMPLX_1:62
.= (i*2*(1-i)*|.fx.| + r0) / t;
then i+c-1 = (i*2*(1-i)*|.fx.|+r0) / t - t / t by A6,A9,XCMPLX_1:60
.= (i*2*(1-i)*|.fx.|+r0 - t) / t by XCMPLX_1:120;
then
A11: i+c-1+1 <= 0+1 by A6,A9,A10,XREAL_1:7;
set X1 = ]. i-c, i+c .[;
set X2 = X1 /\ I;
reconsider X2 as Subset of I[01] by XBOOLE_1:17;
reconsider B = Ball(lx,r0/2/(1-i)) as Subset of TOP-REAL n by TOPREAL3:8;
take W = [:B,X2:];
0 < (1-i)*r0 by A6,A9,XREAL_1:129;
then
A12: 0 < c by A6,A9,XREAL_1:139;
then |.i-i.| < c by ABSVALUE:def 1;
then i in X1 by RCOMP_1:1;
then
A13: i in X2 by XBOOLE_0:def 4;
0 <= i by BORSUK_1:43;
then
A14: i+c is Point of I[01] by A6,A9,A11,BORSUK_1:43;
A15: now
per cases;
suppose
A16: 0 <= i-c;
X1 c= the carrier of I[01]
proof
let a be object;
assume
A17: a in X1;
then reconsider a as Real;
a < i+c by A17,XXREAL_1:4;
then
A18: a < 1 by A11,XXREAL_0:2;
0 < a by A16,A17,XXREAL_1:4;
hence thesis by A18,BORSUK_1:43;
end;
then reconsider X1 as Subset of I[01];
now
per cases;
suppose
i-c <= i+c;
then i-c <= 1 by A11,XXREAL_0:2;
then i-c is Point of I[01] by A16,BORSUK_1:43;
hence X1 is open by A14,BORSUK_4:45;
end;
suppose
i-c > i+c;
then X1 = {}I[01] by XXREAL_1:28;
hence X1 is open;
end;
end;
hence X2 is open by A3;
end;
suppose
A19: i-c < 0;
X2 = [. 0, i+c .[
proof
hereby
let a be object;
assume
A20: a in X2;
then reconsider b = a as Real;
a in X1 by A20,XBOOLE_0:def 4;
then
A21: b < i+c by XXREAL_1:4;
0 <= b by A20,BORSUK_1:43;
hence a in [. 0,i+c.[ by A21,XXREAL_1:3;
end;
let a be object;
assume
A22: a in [. 0,i+c .[;
then reconsider b = a as Real;
A23: 0 <= b by A22,XXREAL_1:3;
A24: b < i+c by A22,XXREAL_1:3;
then b <= 1 by A11,XXREAL_0:2;
then
A25: a in I by A23,BORSUK_1:40,XXREAL_1:1;
a in X1 by A19,A24,A23,XXREAL_1:4;
hence thesis by A25,XBOOLE_0:def 4;
end;
hence X2 is open by A14,Th5;
end;
end;
x in B by A8,A9,GOBOARD6:1,XREAL_1:139;
hence p in W by A4,A13,ZFMISC_1:87;
B is open by GOBOARD6:3;
hence W is open by A15,BORSUK_1:6;
A26: 0 < 2*(1-i) by A9,XREAL_1:129;
F.:W c= Ball(ep,r0)
proof
let m be object;
assume m in F.:W;
then consider z being object such that
A27: z in dom F and
A28: z in W and
A29: F.z = m by FUNCT_1:def 6;
reconsider z as Point of [:TOP-REAL n,I[01]:] by A27;
consider y being Point of TOP-REAL n, j being Point of I[01] such that
A30: z = [y,j] by BORSUK_1:10;
reconsider ez = F.z, ey = y as Point of Euclid n by TOPREAL3:8;
reconsider fp = ep, fz = ez, fe = (1-i)*y, fy = y as Element of REAL n
by EUCLID:22;
A31: (1-i) * (r0/(1-i)/2) = r0/2 & r0/2/(1-i) = r0/(1-i)/2 by A9,
XCMPLX_1:48,97;
fy in B by A28,A30,ZFMISC_1:87;
then
A32: dist(lx,ey) < r0/2/(1-i) by METRIC_1:11;
j in X2 by A28,A30,ZFMISC_1:87;
then j in X1 by XBOOLE_0:def 4;
then |.j-i.| < c by RCOMP_1:1;
then |.i-j.| < c by UNIFORM1:11;
then
A33: |.i-j.|*|.fy.| <= c*|.fy.| by XREAL_1:64;
reconsider yy=ey as Element of n-tuples_on REAL by A2,EUCLID:22;
ez = F.(y,j) by A30
.= (1-j)*y by A1;
then fe-fz = (1-i)*yy -(1-j)*yy;
then
A34: |.fe-fz.| = |.(1-i-(1-j))*fy.| by Th8
.= |.j-i.|*|.fy.| by EUCLID:11
.= |.i-j.|*|.fy.| by UNIFORM1:11;
reconsider gx = fx, gy=fy as Element of n-tuples_on REAL by
EUCLID:def 1;
A35: dist(ep,ez) = |.fp-fz.| & |.fp-fz.| <= |.fp-fe.| + |.fe-fz.| by
EUCLID:19,SPPOL_1:5;
A36: (1-i)*(fx-fy) = (1-i)*(gx-gy) .= (1-i)*gx-(1-i)*gy by Th7
.= (1-i)*fx-(1-i)*fy
.= (1-i)*fx-fe;
A37: dist(lx,ey) = |.fx-fy.| by SPPOL_1:5;
then (1-i) * |.fx-fy.| < (1-i) * (r0/2/(1-i)) by A9,A32,XREAL_1:68;
then |.1-i.| * |.fx-fy.| < r0/2 by A9,A31,ABSVALUE:def 1;
then
A38: |.(1-i)*fx-fe.| < r0/2 by A36,EUCLID:11;
|.fx-fy.| = |.fy-fx.| & |.fy.| - |.fx.| <= |.fy-fx.| by EUCLID:15,18;
then |.fy.| - |.fx.| < r0/2/(1-i) by A32,A37,XXREAL_0:2;
then |.fy.| < |.fx.| + r0/2/(1-i) by XREAL_1:19;
then
A39: c*|.fy.| < c * (|.fx.| + r0/2/(1-i)) by A12,XREAL_1:68;
c * (|.fx.| + r0/2/(1-i)) = c * (|.fx.| + r0/(2*(1-i))) by XCMPLX_1:78
.= c * ((|.fx.|*(2*(1-i)))/(2*(1-i))+r0/(2*(1-i))) by A26,XCMPLX_1:89
.= c * ((|.fx.|*(2*(1-i))+r0)/(2*(1-i))) by XCMPLX_1:62
.= (1-i)*r0 / (2*(1-i)) by A6,A9,XCMPLX_1:98
.= r0/2 by A9,XCMPLX_1:91;
then
A40: |.i-j.|*|.fy.| <= r0/2 by A33,A39,XXREAL_0:2;
fp = (1-i)*x by A5
.= (1-i)*fx;
then |.fp-fe.| + |.fe-fz.| < r0/2 + r0/2 by A34,A40,A38,XREAL_1:8;
then dist(ep,ez) < r0 by A35,XXREAL_0:2;
hence thesis by A29,METRIC_1:11;
end;
hence thesis by A7;
end;
suppose
A41: 1-i <= 0;
A42: i <= 1 by BORSUK_1:43;
1-i+i <= 0+i by A41,XREAL_1:6;
then
A43: i = 1 by A42,XXREAL_0:1;
set t = |.fx.|+r0;
reconsider B = Ball(lx,r0) as Subset of TOP-REAL n by TOPREAL3:8;
set c = r0 / t;
set X1 = ]. 1-c, 1 .];
A44: x in B by A6,GOBOARD6:1;
0+r0 <= t by XREAL_1:7;
then
A45: c <= 1 by A6,XREAL_1:185;
then
A46: c-c <= 1-c by XREAL_1:9;
X1 c= I
proof
let s be object;
assume
A47: s in X1;
then reconsider s as Real;
s <= 1 & 1-c < s by A47,XXREAL_1:2;
hence thesis by A46,BORSUK_1:43;
end;
then reconsider X1 as Subset of I[01];
c is Point of I[01] by A6,A45,BORSUK_1:43;
then 1-c is Point of I[01] by JORDAN5B:4;
then
A48: X1 is open by Th4;
take W = [:B,X1:];
A49: 0 < c by A6,XREAL_1:139;
then 1-c < 1-0 by XREAL_1:15;
then i in X1 by A43,XXREAL_1:2;
hence p in W by A4,A44,ZFMISC_1:87;
B is open by GOBOARD6:3;
hence W is open by A48,BORSUK_1:6;
F.:W c= Ball(ep,r0)
proof
let m be object;
assume m in F.:W;
then consider z being object such that
A50: z in dom F and
A51: z in W and
A52: F.z = m by FUNCT_1:def 6;
reconsider z as Point of [:TOP-REAL n,I[01]:] by A50;
consider y being Point of TOP-REAL n, j being Point of I[01] such that
A53: z = [y,j] by BORSUK_1:10;
reconsider ez = F.z, ey = y as Point of Euclid n by TOPREAL3:8;
reconsider fp = ep, fz = ez, fy = y as Element of REAL n by EUCLID:22;
fy in B by A51,A53,ZFMISC_1:87;
then
A54: dist(lx,ey) < r0 by METRIC_1:11;
A55: ez = F.(y,j) by A53
.= (1-j)*y by A1;
fp = (1-i)*x by A5
.= 0.TOP-REAL n by A43,RLVECT_1:10;
then
A56: fz-fp = F.z - 0.TOP-REAL n
.= fz by RLVECT_1:13;
A57: |.fy.| - |.fx.| <= |.fy-fx.| by EUCLID:15;
dist(lx,ey) = |.fx-fy.| & |.fx-fy.| = |.fy-fx.| by EUCLID:18
,SPPOL_1:5;
then |.fy.| - |.fx.| < r0 by A54,A57,XXREAL_0:2;
then
A58: |.fy.| < t by XREAL_1:19;
A59: now
per cases;
suppose
j < 1;
then
A60: j-j < 1-j by XREAL_1:14;
j in X1 by A51,A53,ZFMISC_1:87;
then 1-c < j by XXREAL_1:2;
then 1-c+c < j+c by XREAL_1:8;
then 1-j < j+c-j by XREAL_1:14;
then r0/(1-j) > r0/c by A6,A60,XREAL_1:76;
then t < r0/(1-j) by A49,XCMPLX_1:54;
then |.fy.| < r0/(1-j) by A58,XXREAL_0:2;
then (1-j)*|.fy.| < (1-j)*(r0/(1-j)) by A60,XREAL_1:68;
hence (1-j)*|.fy.| < r0 by A60,XCMPLX_1:87;
end;
suppose
A61: j >= 1;
j <= 1 by BORSUK_1:43;
then j = 1 by A61,XXREAL_0:1;
hence (1-j)*|.fy.| < r0 by A6;
end;
end;
1-j is Point of I[01] by JORDAN5B:4;
then
A62: 0 <= 1-j by BORSUK_1:43;
dist(ep,ez) = |.fz-fp.| by SPPOL_1:5
.= |.fz.| by A56
.= |.(1-j)*fy.| by A55
.= |.1-j.|*|.fy.| by EUCLID:11
.= (1-j)*|.fy.| by A62,ABSVALUE:def 1;
hence thesis by A52,A59,METRIC_1:11;
end;
hence thesis by A7;
end;
end;
hence thesis by JGRAPH_2:10;
end;
theorem Th18:
for F being Function of [:TOP-REAL n,I[01]:], TOP-REAL n st for
x being Point of TOP-REAL n, i being Point of I[01] holds F.(x,i) = i * x holds
F is continuous
proof
set I = the carrier of I[01];
let F be Function of [:TOP-REAL n,I[01]:], TOP-REAL n such that
A1: for x being Point of TOP-REAL n, i being Point of I[01] holds F.(x,i
) = i * x;
A2: REAL n = n-tuples_on REAL by EUCLID:def 1;
A3: [#]I[01] = I;
for p being Point of [:TOP-REAL n,I[01]:], V being Subset of TOP-REAL n
st F.p in V & V is open ex W being Subset of [:TOP-REAL n,I[01]:] st p in W & W
is open & F.:W c= V
proof
let p be Point of [:TOP-REAL n,I[01]:], V be Subset of TOP-REAL n;
reconsider ep = F.p as Point of Euclid n by TOPREAL3:8;
consider x being Point of TOP-REAL n, i being Point of I[01] such that
A4: p = [x,i] by BORSUK_1:10;
A5: ep = F.(x,i) by A4
.= i*x by A1;
reconsider fx = x as Element of REAL n by EUCLID:22;
reconsider lx = x as Point of Euclid n by TOPREAL3:8;
assume F.p in V & V is open;
then F.p in Int V by TOPS_1:23;
then consider r0 being Real such that
A6: r0 > 0 and
A7: Ball(ep,r0) c= V by GOBOARD6:5;
A8: r0/2 > 0 by A6,XREAL_1:139;
per cases;
suppose
A9: i > 0;
set t = 2*i*|.fx.|+r0;
set c = i*r0 / t;
i <= 1 by BORSUK_1:43;
then 1-1 >= i-1 by XREAL_1:9;
then 2*i*|.fx.| * (i-1) <= 0 by A9;
then
A10: i*(2*i*|.fx.|) - 2*i*|.fx.| - r0 < r0 - r0 by A6;
A11: i-c = i*t/t - (i*r0 / t) by A6,A9,XCMPLX_1:89
.= (i*t - i*r0) / t by XCMPLX_1:120
.= i*(2*i*|.fx.|) / t;
then i-c-1 = i*(2*i*|.fx.|) / t - t / t by A6,A9,XCMPLX_1:60
.= (i*(2*i*|.fx.|) - t) / t by XCMPLX_1:120;
then i-c-1 < 0 by A6,A9,A10,XREAL_1:141;
then i-c-1+1 < 0+1 by XREAL_1:8;
then
A12: i-c is Point of I[01] by A6,A9,A11,BORSUK_1:43;
set X1 = ]. i-c, i+c .[;
set X2 = X1 /\ I;
reconsider X2 as Subset of I[01] by XBOOLE_1:17;
reconsider B = Ball(lx,r0/2/i) as Subset of TOP-REAL n by TOPREAL3:8;
take W = [:B,X2:];
0 < i*r0 by A6,A9,XREAL_1:129;
then
A13: 0 < c by A6,A9,XREAL_1:139;
then |.i-i.| < c by ABSVALUE:def 1;
then i in X1 by RCOMP_1:1;
then
A14: i in X2 by XBOOLE_0:def 4;
A15: 0 <= i-c by A6,A9,A11;
A16: now
per cases;
suppose
A17: i+c <= 1;
X1 c= the carrier of I[01]
proof
let a be object;
assume
A18: a in X1;
then reconsider a as Real;
a < i+c by A18,XXREAL_1:4;
then
A19: a < 1 by A17,XXREAL_0:2;
0 < a by A6,A9,A11,A18,XXREAL_1:4;
hence thesis by A19,BORSUK_1:43;
end;
then reconsider X1 as Subset of I[01];
i+c is Point of I[01] by A6,A9,A17,BORSUK_1:43;
then X1 is open by A12,BORSUK_4:45;
hence X2 is open by A3;
end;
suppose
A20: i+c > 1;
X2 = ]. i-c, 1 .]
proof
hereby
let a be object;
assume
A21: a in X2;
then reconsider b = a as Real;
a in X1 by A21,XBOOLE_0:def 4;
then
A22: i-c < b by XXREAL_1:4;
b <= 1 by A21,BORSUK_1:43;
hence a in ]. i-c, 1 .] by A22,XXREAL_1:2;
end;
let a be object;
assume
A23: a in ]. i-c, 1 .];
then reconsider b = a as Real;
A24: i-c < b by A23,XXREAL_1:2;
A25: b <= 1 by A23,XXREAL_1:2;
then b < i+c by A20,XXREAL_0:2;
then
A26: a in X1 by A24,XXREAL_1:4;
a in I by A15,A24,A25,BORSUK_1:40,XXREAL_1:1;
hence thesis by A26,XBOOLE_0:def 4;
end;
hence X2 is open by A12,Th4;
end;
end;
x in B by A8,A9,GOBOARD6:1,XREAL_1:139;
hence p in W by A4,A14,ZFMISC_1:87;
B is open by GOBOARD6:3;
hence W is open by A16,BORSUK_1:6;
A27: 0 < 2*i by A9,XREAL_1:129;
F.:W c= Ball(ep,r0)
proof
let m be object;
assume m in F.:W;
then consider z being object such that
A28: z in dom F and
A29: z in W and
A30: F.z = m by FUNCT_1:def 6;
reconsider z as Point of [:TOP-REAL n,I[01]:] by A28;
consider y being Point of TOP-REAL n, j being Point of I[01] such that
A31: z = [y,j] by BORSUK_1:10;
reconsider ez = F.z, ey = y as Point of Euclid n by TOPREAL3:8;
reconsider fp = ep, fz = ez, fe = i*y, fy = y as Element of REAL n by
EUCLID:22;
A32: i * (r0/i/2) = r0/2 & r0/2/i = r0/i/2 by A9,XCMPLX_1:48,97;
fy in B by A29,A31,ZFMISC_1:87;
then
A33: dist(lx,ey) < r0/2/i by METRIC_1:11;
j in X2 by A29,A31,ZFMISC_1:87;
then j in X1 by XBOOLE_0:def 4;
then |.j-i.| < c by RCOMP_1:1;
then |.i-j.| < c by UNIFORM1:11;
then
A34: |.i-j.|*|.fy.| <= c*|.fy.| by XREAL_1:64;
reconsider yy=ey as Element of n-tuples_on REAL by A2,EUCLID:22;
ez = F.(y,j) by A31
.= j*y by A1;
then fe-fz = i*yy -j*yy;
then
A35: |.fe-fz.| = |.(i-j)*fy.| by Th8
.= |.i-j.|*|.fy.| by EUCLID:11;
reconsider yy=y as Element of n-tuples_on REAL by A2,EUCLID:22;
A36: dist(ep,ez) = |.fp-fz.| & |.fp-fz.| <= |.fp-fe.| + |.fe-fz.| by
EUCLID:19,SPPOL_1:5;
A37: dist(lx,ey) = |.fx-fy.| by SPPOL_1:5;
then i * |.fx-fy.| < i * (r0/2/i) by A9,A33,XREAL_1:68;
then
A38: |.i.| * |.fx-fy.| < r0/2 by A9,A32,ABSVALUE:def 1;
|.fx-fy.| = |.fy-fx.| & |.fy.| - |.fx.| <= |.fy-fx.| by EUCLID:15,18;
then |.fy.| - |.fx.| < r0/2/i by A33,A37,XXREAL_0:2;
then |.fy.| < |.fx.| + r0/2/i by XREAL_1:19;
then
A39: c*|.fy.| < c * (|.fx.| + r0/2/i) by A13,XREAL_1:68;
c * (|.fx.| + r0/2/i) = c * (|.fx.| + r0/(2*i)) by XCMPLX_1:78
.= c * ((|.fx.|*(2*i))/(2*i)+r0/(2*i)) by A27,XCMPLX_1:89
.= c * ((|.fx.|*(2*i)+r0)/(2*i)) by XCMPLX_1:62
.= i*r0 / (2*i) by A6,A9,XCMPLX_1:98
.= r0/2 by A9,XCMPLX_1:91;
then
A40: |.i-j.|*|.fy.| <= r0/2 by A34,A39,XXREAL_0:2;
i*fx-fe = i*fx-i*yy
.= i*(fx-fy) by Th7;
then
A41: |.i*fx-fe.| < r0/2 by A38,EUCLID:11;
i*fx-fe = fp-fe by A5;
then |.fp-fe.| + |.fe-fz.| < r0/2 + r0/2 by A35,A40,A41,XREAL_1:8;
then dist(ep,ez) < r0 by A36,XXREAL_0:2;
hence thesis by A30,METRIC_1:11;
end;
hence thesis by A7;
end;
suppose
A42: i <= 0;
set t = |.fx.|+r0;
reconsider B = Ball(lx,r0) as Subset of TOP-REAL n by TOPREAL3:8;
set c = r0 / t;
set X1 = [. 0, c .[;
A43: 0 < c by A6,XREAL_1:139;
0+r0 <= t by XREAL_1:7;
then
A44: c <= 1 by A6,XREAL_1:185;
A45: X1 c= I
proof
let s be object;
assume
A46: s in X1;
then reconsider s as Real;
s < c by A46,XXREAL_1:3;
then
A47: s <= 1 by A44,XXREAL_0:2;
0 <= s by A46,XXREAL_1:3;
hence thesis by A47,BORSUK_1:43;
end;
A48: B is open by GOBOARD6:3;
reconsider X1 as Subset of I[01] by A45;
take W = [:B,X1:];
A49: x in B by A6,GOBOARD6:1;
A50: i = 0 by A42,BORSUK_1:43;
then i in X1 by A43,XXREAL_1:3;
hence p in W by A4,A49,ZFMISC_1:87;
c is Point of I[01] by A6,A44,BORSUK_1:43;
then X1 is open by Th5;
hence W is open by A48,BORSUK_1:6;
F.:W c= Ball(ep,r0)
proof
let m be object;
assume m in F.:W;
then consider z being object such that
A51: z in dom F and
A52: z in W and
A53: F.z = m by FUNCT_1:def 6;
reconsider z as Point of [:TOP-REAL n,I[01]:] by A51;
consider y being Point of TOP-REAL n, j being Point of I[01] such that
A54: z = [y,j] by BORSUK_1:10;
reconsider ez = F.z, ey = y as Point of Euclid n by TOPREAL3:8;
reconsider fp = ep, fz = ez, fy = y as Element of REAL n by EUCLID:22;
fy in B by A52,A54,ZFMISC_1:87;
then
A55: dist(lx,ey) < r0 by METRIC_1:11;
A56: ez = F.(y,j) by A54
.= j*y by A1;
fp = i*x by A5
.= 0.TOP-REAL n by A50,RLVECT_1:10;
then
A57: fz-fp = F.z - 0.TOP-REAL n
.= fz by RLVECT_1:13;
A58: |.fy.| - |.fx.| <= |.fy-fx.| by EUCLID:15;
dist(lx,ey) = |.fx-fy.| & |.fx-fy.| = |.fy-fx.| by EUCLID:18
,SPPOL_1:5;
then |.fy.| - |.fx.| < r0 by A55,A58,XXREAL_0:2;
then
A59: |.fy.| < t by XREAL_1:19;
A60: now
per cases;
suppose
A61: 0 < j;
j in X1 by A52,A54,ZFMISC_1:87;
then j < c by XXREAL_1:3;
then r0/j > r0/c by A6,A61,XREAL_1:76;
then t < r0/j by A43,XCMPLX_1:54;
then |.fy.| < r0/j by A59,XXREAL_0:2;
then j*|.fy.| < j*(r0/j) by A61,XREAL_1:68;
hence j*|.fy.| < r0 by A61,XCMPLX_1:87;
end;
suppose
j <= 0;
hence j*|.fy.| < r0 by A6;
end;
end;
A62: 0 <= j by BORSUK_1:43;
dist(ep,ez) = |.fz-fp.| by SPPOL_1:5
.= |.fz.| by A57
.= |.j*fy.| by A56
.= |.j.|*|.fy.| by EUCLID:11
.= j*|.fy.| by A62,ABSVALUE:def 1;
hence thesis by A53,A60,METRIC_1:11;
end;
hence thesis by A7;
end;
end;
hence thesis by JGRAPH_2:10;
end;
begin :: Paths
reserve X for non empty TopSpace,
a, b, c, d, e, f for Point of X,
T for non empty pathwise_connected TopSpace,
a1, b1, c1, d1, e1, f1 for Point of T;
theorem Th19:
a,b are_connected & b,c are_connected implies for A1,A2 being
Path of a,b, B being Path of b,c holds A1,A2 are_homotopic implies A1, A2+B+-B
are_homotopic
proof
assume that
A1: a,b are_connected and
A2: b,c are_connected;
set X = the constant Path of b,b;
let A1,A2 be Path of a,b, B be Path of b,c;
A3: A1, A1+X are_homotopic by A1,BORSUK_6:80;
assume
A4: A1, A2 are_homotopic;
B+-B, X are_homotopic by A2,BORSUK_6:84;
then A2+(B+-B), A1+X are_homotopic by A1,A4,BORSUK_6:75;
then
A5: A2+(B+-B), A1 are_homotopic by A3,BORSUK_6:79;
A2+(B+-B), A2+B+-B are_homotopic by A1,A2,BORSUK_6:73;
hence thesis by A5,BORSUK_6:79;
end;
theorem
for A1,A2 being Path of a1,b1, B being Path of b1,c1 holds A1,A2
are_homotopic implies A1, A2+B+-B are_homotopic
proof
let A1,A2 be Path of a1,b1;
a1,b1 are_connected & b1,c1 are_connected by BORSUK_2:def 3;
hence thesis by Th19;
end;
theorem Th21:
a,b are_connected & c,b are_connected implies for A1,A2 being
Path of a,b, B being Path of c,b holds A1,A2 are_homotopic implies A1, A2+-B+B
are_homotopic
proof
assume that
A1: a,b are_connected and
A2: c,b are_connected;
set X = the constant Path of b,b;
let A1,A2 be Path of a,b, B be Path of c,b;
A3: A1, A1+X are_homotopic by A1,BORSUK_6:80;
assume
A4: A1, A2 are_homotopic;
-B+B, X are_homotopic by A2,BORSUK_6:86;
then A2+(-B+B), A1+X are_homotopic by A1,A4,BORSUK_6:75;
then
A5: A2+(-B+B), A1 are_homotopic by A3,BORSUK_6:79;
A2+(-B+B), A2+-B+B are_homotopic by A1,A2,BORSUK_6:73;
hence thesis by A5,BORSUK_6:79;
end;
theorem
for A1,A2 being Path of a1,b1, B being Path of c1,b1 holds A1,A2
are_homotopic implies A1, A2+-B+B are_homotopic
proof
a1,b1 are_connected & c1,b1 are_connected by BORSUK_2:def 3;
hence thesis by Th21;
end;
theorem Th23:
a,b are_connected & c,a are_connected implies for A1,A2 being
Path of a,b, B being Path of c,a holds A1,A2 are_homotopic implies A1, -B+B+A2
are_homotopic
proof
assume that
A1: a,b are_connected and
A2: c,a are_connected;
set X = the constant Path of a,a;
let A1,A2 be Path of a,b, B be Path of c,a;
A3: A1, X+A1 are_homotopic by A1,BORSUK_6:82;
assume
A4: A1, A2 are_homotopic;
-B+B, X are_homotopic by A2,BORSUK_6:86;
then -B+B+A2, X+A1 are_homotopic by A1,A4,BORSUK_6:75;
hence thesis by A3,BORSUK_6:79;
end;
theorem
for A1,A2 being Path of a1,b1, B being Path of c1,a1 holds A1,A2
are_homotopic implies A1, -B+B+A2 are_homotopic
proof
a1,b1 are_connected & c1,a1 are_connected by BORSUK_2:def 3;
hence thesis by Th23;
end;
theorem Th25:
a,b are_connected & a,c are_connected implies for A1,A2 being
Path of a,b, B being Path of a,c holds A1,A2 are_homotopic implies A1, B+-B+A2
are_homotopic
proof
assume that
A1: a,b are_connected and
A2: a,c are_connected;
set X = the constant Path of a,a;
let A1,A2 be Path of a,b, B be Path of a,c;
A3: A1, X+A1 are_homotopic by A1,BORSUK_6:82;
assume
A4: A1, A2 are_homotopic;
B+-B, X are_homotopic by A2,BORSUK_6:84;
then B+-B+A2, X+A1 are_homotopic by A1,A4,BORSUK_6:75;
hence thesis by A3,BORSUK_6:79;
end;
theorem
for A1,A2 being Path of a1,b1, B being Path of a1,c1 holds A1,A2
are_homotopic implies A1, B+-B+A2 are_homotopic
proof
a1,b1 are_connected & a1,c1 are_connected by BORSUK_2:def 3;
hence thesis by Th25;
end;
theorem Th27:
a,b are_connected & c,b are_connected implies for A, B being
Path of a,b, C being Path of b,c st A+C, B+C are_homotopic holds A, B
are_homotopic
proof
assume that
A1: a,b are_connected and
A2: c,b are_connected;
let A, B be Path of a,b, C be Path of b,c;
A3: A+C+-C, A are_homotopic by A1,A2,Th19,BORSUK_2:12;
assume
A4: A+C, B+C are_homotopic;
a,c are_connected & -C, -C are_homotopic by A1,A2,BORSUK_2:12,BORSUK_6:42;
then A+C+-C, B+C+-C are_homotopic by A2,A4,BORSUK_6:75;
then
A5: A, B+C+-C are_homotopic by A3,BORSUK_6:79;
B+C+-C, B are_homotopic by A1,A2,Th19,BORSUK_2:12;
hence thesis by A5,BORSUK_6:79;
end;
theorem
for A, B being Path of a1,b1, C being Path of b1,c1 st A+C, B+C
are_homotopic holds A, B are_homotopic
proof
a1,b1 are_connected & c1,b1 are_connected by BORSUK_2:def 3;
hence thesis by Th27;
end;
theorem Th29:
a,b are_connected & a,c are_connected implies for A, B being
Path of a,b, C being Path of c,a st C+A, C+B are_homotopic holds A, B
are_homotopic
proof
assume that
A1: a,b are_connected and
A2: a,c are_connected;
let A, B be Path of a,b, C be Path of c,a;
A3: -C+C+A, -C+(C+A) are_homotopic by A1,A2,BORSUK_6:73;
assume
A4: C+A, C+B are_homotopic;
b,c are_connected & -C, -C are_homotopic by A1,A2,BORSUK_2:12,BORSUK_6:42;
then -C+(C+A), -C+(C+B) are_homotopic by A2,A4,BORSUK_6:75;
then
A5: -C+C+A, -C+(C+B) are_homotopic by A3,BORSUK_6:79;
-C+C+B, -C+(C+B) are_homotopic by A1,A2,BORSUK_6:73;
then
A6: -C+C+A, -C+C+B are_homotopic by A5,BORSUK_6:79;
-C+C+A, A are_homotopic by A1,A2,Th23,BORSUK_2:12;
then
A7: A, -C+C+B are_homotopic by A6,BORSUK_6:79;
-C+C+B, B are_homotopic by A1,A2,Th23,BORSUK_2:12;
hence thesis by A7,BORSUK_6:79;
end;
theorem
for A, B being Path of a1,b1, C being Path of c1,a1 st C+A, C+B
are_homotopic holds A, B are_homotopic
proof
a1,b1 are_connected & a1,c1 are_connected by BORSUK_2:def 3;
hence thesis by Th29;
end;
theorem Th31:
a,b are_connected & b,c are_connected & c,d are_connected & d,e
are_connected implies for A being Path of a,b, B being Path of b,c, C being
Path of c,d, D being Path of d,e holds A+B+C+D, A+(B+C)+D are_homotopic
proof
assume that
A1: a,b are_connected & b,c are_connected and
A2: c,d are_connected and
A3: d,e are_connected;
a,c are_connected by A1,BORSUK_6:42;
then
A4: a,d are_connected by A2,BORSUK_6:42;
let A be Path of a,b, B be Path of b,c, C be Path of c,d, D be Path of d,e;
A+B+C, A+(B+C) are_homotopic & D, D are_homotopic by A1,A2,A3,BORSUK_2:12
,BORSUK_6:73;
hence thesis by A3,A4,BORSUK_6:75;
end;
theorem
for A being Path of a1,b1, B being Path of b1,c1, C being Path of c1,
d1, D being Path of d1,e1 holds A+B+C+D, A+(B+C)+D are_homotopic
proof
A1: c1,d1 are_connected & d1,e1 are_connected by BORSUK_2:def 3;
a1,b1 are_connected & b1,c1 are_connected by BORSUK_2:def 3;
hence thesis by A1,Th31;
end;
theorem Th33:
a,b are_connected & b,c are_connected & c,d are_connected & d,e
are_connected implies for A being Path of a,b, B being Path of b,c, C being
Path of c,d, D being Path of d,e holds A+B+C+D, A+(B+C+D) are_homotopic
proof
assume that
A1: a,b are_connected and
A2: b,c are_connected & c,d are_connected and
A3: d,e are_connected;
let A be Path of a,b, B be Path of b,c, C be Path of c,d, D be Path of d,e;
A4: A+(B+C), A+B+C are_homotopic & D, D are_homotopic by A1,A2,A3,BORSUK_2:12
,BORSUK_6:73;
A5: b,d are_connected by A2,BORSUK_6:42;
then a,d are_connected by A1,BORSUK_6:42;
then
A6: A+(B+C)+D, A+B+C+D are_homotopic by A3,A4,BORSUK_6:75;
A+(B+C)+D, A+(B+C+D) are_homotopic by A1,A3,A5,BORSUK_6:73;
hence thesis by A6,BORSUK_6:79;
end;
theorem
for A being Path of a1,b1, B being Path of b1,c1, C being Path of c1,
d1, D being Path of d1,e1 holds A+B+C+D, A+(B+C+D) are_homotopic
proof
A1: c1,d1 are_connected & d1,e1 are_connected by BORSUK_2:def 3;
a1,b1 are_connected & b1,c1 are_connected by BORSUK_2:def 3;
hence thesis by A1,Th33;
end;
theorem Th35:
a,b are_connected & b,c are_connected & c,d are_connected & d,e
are_connected implies for A being Path of a,b, B being Path of b,c, C being
Path of c,d, D being Path of d,e holds A+(B+C)+D, A+B+(C+D) are_homotopic
proof
assume that
A1: a,b are_connected & b,c are_connected and
A2: c,d are_connected & d,e are_connected;
let A be Path of a,b, B be Path of b,c, C be Path of c,d, D be Path of d,e;
a,c are_connected by A1,BORSUK_6:42;
then
A3: A+B+C+D, A+B+(C+D) are_homotopic by A2,BORSUK_6:73;
A+B+C+D, A+(B+C)+D are_homotopic by A1,A2,Th31;
hence thesis by A3,BORSUK_6:79;
end;
theorem
for A being Path of a1,b1, B being Path of b1,c1, C being Path of c1,
d1, D being Path of d1,e1 holds A+(B+C)+D, A+B+(C+D) are_homotopic
proof
A1: c1,d1 are_connected & d1,e1 are_connected by BORSUK_2:def 3;
a1,b1 are_connected & b1,c1 are_connected by BORSUK_2:def 3;
hence thesis by A1,Th35;
end;
theorem Th37:
a,b are_connected & b,c are_connected & b,d are_connected
implies for A being Path of a,b, B being Path of d,b, C being Path of b,c holds
A+-B+B+C, A+C are_homotopic
proof
assume that
A1: a,b are_connected and
A2: b,c are_connected and
A3: b,d are_connected;
let A be Path of a,b, B be Path of d,b, C be Path of b,c;
A4: A+-B+B+C, A+(-B+B+C) are_homotopic by A1,A2,A3,Th33;
set X = the constant Path of b,b;
C,C are_homotopic & -B+B, X are_homotopic by A2,A3,BORSUK_2:12,BORSUK_6:86;
then
A5: -B+B+C, X+C are_homotopic by A2,BORSUK_6:75;
X+C, C are_homotopic by A2,BORSUK_6:82;
then
A6: -B+B+C, C are_homotopic by A5,BORSUK_6:79;
A,A are_homotopic by A1,BORSUK_2:12;
then A+(-B+B+C), A+C are_homotopic by A1,A2,A6,BORSUK_6:75;
hence thesis by A4,BORSUK_6:79;
end;
theorem
for A being Path of a1,b1, B being Path of d1,b1, C being Path of b1,
c1 holds A+-B+B+C, A+C are_homotopic
proof
A1: b1,d1 are_connected by BORSUK_2:def 3;
a1,b1 are_connected & b1,c1 are_connected by BORSUK_2:def 3;
hence thesis by A1,Th37;
end;
theorem Th39:
a,b are_connected & a,c are_connected & c,d are_connected
implies for A being Path of a,b, B being Path of c,d, C being Path of a,c holds
A+-A+C+B+-B, C are_homotopic
proof
assume that
A1: a,b are_connected and
A2: a,c are_connected and
A3: c,d are_connected;
let A be Path of a,b, B be Path of c,d, C be Path of a,c;
B+-B, B+-B are_homotopic & A+-A+C, C are_homotopic by A1,A2,Th25,BORSUK_2:12;
then
A4: A+-A+C+(B+-B), C+(B+-B) are_homotopic by A2,BORSUK_6:75;
C, C+B+-B are_homotopic & C+B+-B, C+(B+-B) are_homotopic by A2,A3,Th19,
BORSUK_2:12,BORSUK_6:73;
then
A5: C, C+(B+-B) are_homotopic by BORSUK_6:79;
A+-A+C+B+-B, A+-A+C+(B+-B) are_homotopic by A2,A3,BORSUK_6:73;
then A+-A+C+B+-B, C+(B+-B) are_homotopic by A4,BORSUK_6:79;
hence thesis by A5,BORSUK_6:79;
end;
theorem
for A being Path of a1,b1, B being Path of c1,d1, C being Path of a1,
c1 holds A+-A+C+B+-B, C are_homotopic
proof
A1: c1,d1 are_connected by BORSUK_2:def 3;
a1,b1 are_connected & a1,c1 are_connected by BORSUK_2:def 3;
hence thesis by A1,Th39;
end;
theorem Th41:
a,b are_connected & a,c are_connected & d,c are_connected
implies for A being Path of a,b, B being Path of c,d, C being Path of a,c holds
A+(-A+C+B)+-B, C are_homotopic
proof
assume that
A1: a,b are_connected & a,c are_connected and
A2: d,c are_connected;
let A be Path of a,b, B be Path of c,d, C be Path of a,c;
A3: A+-A+C+B+-B, C are_homotopic by A1,A2,Th39;
A4: -B, -B are_homotopic by A2,BORSUK_2:12;
A+(-A+C+B), A+-A+C+B are_homotopic & a,d are_connected by A1,A2,Th33,
BORSUK_6:42;
then A+(-A+C+B)+-B, A+-A+C+B+-B are_homotopic by A2,A4,BORSUK_6:75;
hence thesis by A3,BORSUK_6:79;
end;
theorem
for A being Path of a1,b1, B being Path of c1,d1, C being Path of a1,
c1 holds A+(-A+C+B)+-B, C are_homotopic
proof
A1: a1,c1 are_connected by BORSUK_2:def 3;
a1,b1 are_connected & d1,c1 are_connected by BORSUK_2:def 3;
hence thesis by A1,Th41;
end;
theorem Th43:
a,b are_connected & b,c are_connected & c,d are_connected & d,e
are_connected & a,f are_connected implies for A being Path of a,b, B being Path
of b,c, C being Path of c,d, D being Path of d,e, E being Path of f,c holds A+(
B+C)+D, A+B+-E+(E+C+D) are_homotopic
proof
assume that
A1: a,b are_connected & b,c are_connected and
A2: c,d are_connected & d,e are_connected and
A3: a,f are_connected;
let A be Path of a,b, B be Path of b,c, C be Path of c,d, D be Path of d,e,
E be Path of f,c;
A4: A+B+-E, A+B+-E are_homotopic by A3,BORSUK_2:12;
A5: a,c are_connected by A1,BORSUK_6:42;
then
A6: f,c are_connected by A3,BORSUK_6:42;
then
A7: E+(C+D), E+C+D are_homotopic by A2,BORSUK_6:73;
A8: c,e are_connected by A2,BORSUK_6:42;
then
A9: A+B+-E+(E+(C+D)), A+B+-E+E+(C+D) are_homotopic by A3,A6,BORSUK_6:73;
A10: A+B+(C+D), A+(B+C)+D are_homotopic by A1,A2,Th35;
f,e are_connected by A8,A6,BORSUK_6:42;
then A+B+-E+(E+(C+D)), A+B+-E+(E+C+D) are_homotopic by A3,A7,A4,BORSUK_6:75;
then
A11: A+B+-E+E+(C+D), A+B+-E+(E+C+D) are_homotopic by A9,BORSUK_6:79;
A+B+-E+E+(C+D), A+B+(C+D) are_homotopic by A5,A8,A6,Th37;
then A+(B+C)+D, A+B+-E+E+(C+D) are_homotopic by A10,BORSUK_6:79;
hence thesis by A11,BORSUK_6:79;
end;
theorem
for A being Path of a1,b1, B being Path of b1,c1, C being Path of c1,
d1, D being Path of d1,e1, E being Path of f1,c1 holds A+(B+C)+D, A+B+-E+(E+C+D
) are_homotopic
proof
A1: c1,d1 are_connected & d1,e1 are_connected by BORSUK_2:def 3;
A2: a1,f1 are_connected by BORSUK_2:def 3;
a1,b1 are_connected & b1,c1 are_connected by BORSUK_2:def 3;
hence thesis by A1,A2,Th43;
end;
begin :: Fundamental group
definition
let T be TopStruct, t be Point of T;
mode Loop of t is Path of t,t;
end;
definition
let T be non empty TopStruct, t1,t2 be Point of T;
defpred P[object] means $1 is Path of t1,t2;
func Paths(t1,t2) -> set means
:Def1:
for x being object holds x in it iff x is Path of t1,t2;
existence
proof
consider X being set such that
A1: for x being object holds x in X iff x in Funcs(the carrier of I[01],
the carrier of T) & P[x] from XBOOLE_0:sch 1;
take X;
let x be object;
thus x in X implies x is Path of t1,t2 by A1;
assume
A2: x is Path of t1,t2;
then x in Funcs(the carrier of I[01],the carrier of T) by FUNCT_2:8;
hence thesis by A1,A2;
end;
uniqueness
proof
thus for X1,X2 being set st
(for x being object holds x in X1 iff P[x]) & (
for x being object holds x in X2 iff P[x]) holds X1 = X2
from XBOOLE_0:sch 3;
end;
end;
registration
let T be non empty TopStruct, t1,t2 be Point of T;
cluster Paths(t1,t2) -> non empty;
coherence
proof
the Path of t1,t2 in Paths(t1,t2) by Def1;
hence thesis;
end;
end;
definition
let T be non empty TopStruct, t be Point of T;
func Loops(t) -> set equals
Paths(t,t);
coherence;
end;
registration
let T be non empty TopStruct, t be Point of T;
cluster Loops(t) -> non empty;
coherence;
end;
Lm2: for X being non empty TopSpace, a,b being Point of X st a,b are_connected
ex E being Equivalence_Relation of Paths(a,b) st
for x,y being object holds [x,y]
in E iff x in Paths(a,b) & y in Paths(a,b) & ex P,Q being Path of a,b st P = x
& Q = y & P,Q are_homotopic
proof
let X be non empty TopSpace, a,b be Point of X such that
A1: a,b are_connected;
defpred P[object,object] means
ex P,Q being Path of a,b st P = $1 & Q = $2 & P,Q
are_homotopic;
A2: for x being object st x in Paths(a,b) holds P[x,x]
proof
let x be object;
assume x in Paths(a,b);
then reconsider x as Path of a,b by Def1;
x,x are_homotopic by A1,BORSUK_2:12;
hence thesis;
end;
A3: for x,y,z being object st P[x,y] & P[y,z] holds P[x,z] by BORSUK_6:79;
A4: for x,y being object st P[x,y] holds P[y,x];
thus ex EqR being Equivalence_Relation of Paths(a,b) st
for x,y being object
holds [x,y] in EqR iff x in Paths(a,b) & y in Paths(a,b) & P[x,y] from EQREL_1:
sch 1(A2,A4,A3);
end;
definition
let X be non empty TopSpace, a,b be Point of X such that
A1: a,b are_connected;
func EqRel(X,a,b) -> Relation of Paths(a,b) means
:Def3:
for P, Q being Path of a,b holds [P,Q] in it iff P,Q are_homotopic;
existence
proof
consider E being Equivalence_Relation of Paths(a,b) such that
A2: for x,y being object holds [x,y] in E iff x in Paths(a,b) & y in
Paths(a,b) & ex P,Q being Path of a,b st P = x & Q = y & P,Q are_homotopic by
A1,Lm2;
take E;
let P, Q be Path of a,b;
thus [P,Q] in E implies P,Q are_homotopic
proof
assume [P,Q] in E;
then
ex P1,Q1 being Path of a,b st P1 = P & Q1 = Q & P1,Q1 are_homotopic
by A2;
hence thesis;
end;
P in Paths(a,b) & Q in Paths(a,b) by Def1;
hence thesis by A2;
end;
uniqueness
proof
let E,F be Relation of Paths(a,b) such that
A3: for P, Q being Path of a,b holds [P,Q] in E iff P,Q are_homotopic and
A4: for P, Q being Path of a,b holds [P,Q] in F iff P,Q are_homotopic;
let x,y be object;
thus [x,y] in E implies [x,y] in F
proof
assume
A5: [x,y] in E;
then x in Paths(a,b) & y in Paths(a,b) by ZFMISC_1:87;
then reconsider x,y as Path of a,b by Def1;
x,y are_homotopic by A3,A5;
hence thesis by A4;
end;
assume
A6: [x,y] in F;
then x in Paths(a,b) & y in Paths(a,b) by ZFMISC_1:87;
then reconsider x,y as Path of a,b by Def1;
x,y are_homotopic by A4,A6;
hence thesis by A3;
end;
end;
Lm3: a,b are_connected implies EqRel(X,a,b) is non empty total symmetric
transitive
proof
set E = EqRel(X,a,b);
set W = Paths(a,b);
assume
A1: a,b are_connected;
then consider EqR being Equivalence_Relation of W such that
A2: for x,y being object holds [x,y] in EqR iff x in W & y in W & ex P,Q
being Path of a,b st P = x & Q = y & P,Q are_homotopic by Lm2;
E = EqR
proof
let x,y be object;
thus [x,y] in E implies [x,y] in EqR
proof
assume
A3: [x,y] in E;
then
A4: x in W & y in W by ZFMISC_1:87;
then reconsider x,y as Path of a,b by Def1;
x,y are_homotopic by A1,A3,Def3;
hence thesis by A2,A4;
end;
assume
A5: [x,y] in EqR;
then x in W & y in W by ZFMISC_1:87;
then reconsider x,y as Path of a,b by Def1;
ex P,Q being Path of a,b st P = x & Q = y & P,Q are_homotopic by A2,A5;
hence thesis by A1,Def3;
end;
hence thesis by EQREL_1:9,RELAT_1:40;
end;
theorem Th45:
a,b are_connected implies for P, Q being Path of a,b holds Q in
Class(EqRel(X,a,b),P) iff P,Q are_homotopic
proof
set E = EqRel(X,a,b);
assume
A1: a,b are_connected;
let P, Q be Path of a,b;
A2: E is non empty total symmetric transitive by A1,Lm3;
hereby
assume Q in Class(E,P);
then [Q,P] in E by A2,EQREL_1:19;
hence P,Q are_homotopic by A1,Def3;
end;
assume P,Q are_homotopic;
then [Q,P] in E by A1,Def3;
hence thesis by A2,EQREL_1:19;
end;
theorem Th46:
a,b are_connected implies for P, Q being Path of a,b holds Class
(EqRel(X,a,b),P) = Class(EqRel(X,a,b),Q) iff P,Q are_homotopic
proof
set E = EqRel(X,a,b);
assume
A1: a,b are_connected;
let P, Q be Path of a,b;
A2: Q in Paths(a,b) by Def1;
A3: E is non empty total symmetric transitive by A1,Lm3;
hereby
assume Class(E,P) = Class(E,Q);
then P in Class(E,Q) by A3,A2,EQREL_1:23;
hence P,Q are_homotopic by A1,Th45;
end;
assume P,Q are_homotopic;
then P in Class(E,Q) by A1,Th45;
hence thesis by A3,A2,EQREL_1:23;
end;
definition
let X be non empty TopSpace, a be Point of X;
func EqRel(X,a) -> Relation of Loops(a) equals
EqRel(X,a,a);
coherence;
end;
registration
let X be non empty TopSpace, a be Point of X;
cluster EqRel(X,a) -> non empty total symmetric transitive;
coherence by Lm3;
end;
definition
let X be non empty TopSpace, a be Point of X;
set E = EqRel(X,a);
set A = Class E;
set W = Loops(a);
func FundamentalGroup(X,a) -> strict multMagma means
:Def5:
the carrier of
it = Class EqRel (X,a) & for x,y being Element of it ex P,Q being Loop of a st
x = Class(EqRel(X,a),P) & y = Class(EqRel(X,a),Q) & (the multF of it).(x,y) =
Class(EqRel(X,a),P+Q);
existence
proof
defpred P[set,set,set] means ex P,Q being Loop of a st $1 = Class(E,P) &
$2 = Class(E,Q) & $3 = Class(E,P+Q);
A1: for x,y being Element of A ex z being Element of A st P[x,y,z]
proof
let x, y be Element of A;
x in A;
then consider P being object such that
A2: P in W and
A3: x = Class(E,P) by EQREL_1:def 3;
y in A;
then consider Q being object such that
A4: Q in W and
A5: y = Class(E,Q) by EQREL_1:def 3;
reconsider P,Q as Loop of a by A2,A4,Def1;
P+Q in W by Def1;
then reconsider z = Class(E,P+Q) as Element of A by EQREL_1:def 3;
take z;
thus thesis by A3,A5;
end;
consider g being BinOp of A such that
A6: for a,b being Element of A holds P[a,b,g.(a,b)] from BINOP_1:sch 3
(A1);
take multMagma(# A,g #);
thus thesis by A6;
end;
uniqueness
proof
let F,G be strict multMagma such that
A7: the carrier of F = Class E and
A8: for x,y being Element of F ex P,Q being Loop of a st x = Class(E,
P) & y = Class(E,Q) & (the multF of F).(x,y) = Class(E,P+Q) and
A9: the carrier of G = A and
A10: for x,y being Element of G ex P,Q being Loop of a st x = Class(E,
P) & y = Class(E,Q) & (the multF of G).(x,y) = Class(E,P+Q);
set g = the multF of G;
set f = the multF of F;
for c,d being Element of F holds f.(c,d) = g.(c,d)
proof
let c,d be Element of F;
consider P1,Q1 being Loop of a such that
A11: c = Class(E,P1) & d = Class(E,Q1) and
A12: f.(c,d) = Class(E,P1+Q1) by A8;
consider P2,Q2 being Loop of a such that
A13: c = Class(E,P2) & d = Class(E,Q2) and
A14: g.(c,d) = Class(E,P2+Q2) by A7,A9,A10;
P1,P2 are_homotopic & Q1,Q2 are_homotopic by A11,A13,Th46;
then P1+Q1,P2+Q2 are_homotopic by BORSUK_6:75;
hence thesis by A12,A14,Th46;
end;
hence thesis by A7,A9,BINOP_1:2;
end;
end;
notation
let X be non empty TopSpace, a be Point of X;
synonym pi_1(X,a) for FundamentalGroup(X,a);
end;
registration
let X be non empty TopSpace;
let a be Point of X;
cluster pi_1(X,a) -> non empty;
coherence
proof
the carrier of pi_1(X,a) = Class EqRel (X,a) by Def5;
hence the carrier of pi_1(X,a) is non empty;
end;
end;
theorem Th47:
for x being set holds x in the carrier of pi_1(X,a) iff ex P
being Loop of a st x = Class(EqRel(X,a),P)
proof
let x be set;
A1: the carrier of pi_1(X,a) = Class EqRel (X,a) by Def5;
hereby
assume x in the carrier of pi_1(X,a);
then consider P being Element of Loops(a) such that
A2: x = Class(EqRel(X,a),P) by A1,EQREL_1:36;
reconsider P as Loop of a by Def1;
take P;
thus x = Class(EqRel(X,a),P) by A2;
end;
given P being Loop of a such that
A3: x = Class(EqRel(X,a),P);
P in Loops(a) by Def1;
hence thesis by A1,A3,EQREL_1:def 3;
end;
Lm4: for S being non empty TopSpace, s being Point of S for x, y being Element
of pi_1(S,s) for P, Q being Loop of s st x = Class(EqRel(S,s),P) & y = Class(
EqRel(S,s),Q) holds x*y = Class(EqRel(S,s),P+Q)
proof
let S be non empty TopSpace;
let s be Point of S;
set X = pi_1(S,s);
let x, y be Element of X;
let P, Q be Loop of s;
consider P1, Q1 being Loop of s such that
A1: x = Class(EqRel(S,s),P1) & y = Class(EqRel(S,s),Q1) and
A2: (the multF of X).(x,y) = Class(EqRel(S,s),P1+Q1) by Def5;
assume x = Class(EqRel(S,s),P) & y = Class(EqRel(S,s),Q);
then P,P1 are_homotopic & Q,Q1 are_homotopic by A1,Th46;
then P+Q,P1+Q1 are_homotopic by BORSUK_6:75;
hence thesis by A2,Th46;
end;
registration
let X be non empty TopSpace;
let a be Point of X;
cluster pi_1(X,a) -> associative Group-like;
coherence
proof
set C = the constant Loop of a;
set E = EqRel(X,a);
set G = pi_1(X,a);
set e = Class(E,C);
C in Loops a by Def1;
then
A1: e in Class E by EQREL_1:def 3;
thus G is associative
proof
let x,y,z be Element of G;
consider A being Loop of a such that
A2: x = Class(E,A) by Th47;
consider B being Loop of a such that
A3: y = Class(E,B) by Th47;
consider BC being Loop of a such that
A4: y*z = Class(E,BC) by Th47;
consider C being Loop of a such that
A5: z = Class(E,C) by Th47;
y*z = Class(E,B+C) by A3,A5,Lm4;
then A,A are_homotopic & BC,B+C are_homotopic by A4,Th46,BORSUK_2:12;
then
A6: A+BC,A+(B+C) are_homotopic by BORSUK_6:75;
consider AB being Loop of a such that
A7: x*y = Class(E,AB) by Th47;
x*y = Class(E,A+B) by A2,A3,Lm4;
then C,C are_homotopic & AB,A+B are_homotopic by A7,Th46,BORSUK_2:12;
then
A8: AB+C,A+B+C are_homotopic by BORSUK_6:75;
A9: A+B+C,A+(B+C) are_homotopic by BORSUK_6:73;
thus (x*y)*z = Class(E,AB+C) by A5,A7,Lm4
.= Class(E,A+B+C) by A8,Th46
.= Class(E,A+(B+C)) by A9,Th46
.= Class(E,A+BC) by A6,Th46
.= x*(y*z) by A2,A4,Lm4;
end;
reconsider e as Element of G by A1,Def5;
take e;
let h be Element of G;
consider A being Loop of a such that
A10: h = Class(E,A) by Th47;
A11: A+C,A are_homotopic by BORSUK_6:80;
thus h * e = Class(E,A+C) by A10,Lm4
.= h by A10,A11,Th46;
A12: C+A,A are_homotopic by BORSUK_6:82;
thus e * h = Class(E,C+A) by A10,Lm4
.= h by A10,A12,Th46;
set x = Class(E,-A);
-A in Loops a by Def1;
then x in Class E by EQREL_1:def 3;
then reconsider x as Element of G by Def5;
take x;
A13: A+-A,C are_homotopic by BORSUK_6:84;
thus h * x = Class(E,A+-A) by A10,Lm4
.= e by A13,Th46;
A14: -A+A,C are_homotopic by BORSUK_6:86;
thus x * h = Class(E,-A+A) by A10,Lm4
.= e by A14,Th46;
end;
end;
definition
let T be non empty TopSpace, x0, x1 be Point of T, P being Path of x0,x1;
assume
A1: x0,x1 are_connected;
func pi_1-iso(P) -> Function of pi_1(T,x1), pi_1(T,x0) means
:Def6:
for Q
being Loop of x1 holds it.Class(EqRel(T,x1),Q) = Class(EqRel(T,x0),P+Q+-P);
existence
proof
defpred P[set,set] means ex L being Loop of x1 st $1 = Class(EqRel(T,x1),L
) & $2 = Class(EqRel(T,x0),P+L+-P);
A2: P,P are_homotopic by A1,BORSUK_2:12;
A3: for x being Element of pi_1(T,x1) ex y being Element of pi_1(T,x0) st
P[x,y]
proof
let x be Element of pi_1(T,x1);
consider Q being Loop of x1 such that
A4: x = Class(EqRel(T,x1),Q) by Th47;
reconsider y = Class(EqRel(T,x0),P+Q+-P) as Element of pi_1(T,x0) by Th47
;
take y;
thus thesis by A4;
end;
consider f being Function of the carrier of pi_1(T,x1), the carrier of
pi_1(T,x0) such that
A5: for x being Element of pi_1(T,x1) holds P[x,f.x] from FUNCT_2:sch
3(A3 );
reconsider f as Function of pi_1(T,x1), pi_1(T,x0);
take f;
let Q be Loop of x1;
the carrier of pi_1(T,x1) = Class EqRel (T,x1) & Q in Loops(x1) by Def1
,Def5;
then Class(EqRel(T,x1),Q) is Element of pi_1(T,x1) by EQREL_1:def 3;
then consider L being Loop of x1 such that
A6: Class(EqRel(T,x1),Q) = Class(EqRel(T,x1),L) and
A7: f.Class(EqRel(T,x1),Q) = Class(EqRel(T,x0),P+L+-P) by A5;
A8: -P,-P are_homotopic by A1,BORSUK_2:12;
L,Q are_homotopic by A6,Th46;
then P+L,P+Q are_homotopic by A1,A2,BORSUK_6:75;
then P+L+-P,P+Q+-P are_homotopic by A1,A8,BORSUK_6:75;
hence thesis by A7,Th46;
end;
uniqueness
proof
let f1, f2 be Function of pi_1(T,x1), pi_1(T,x0) such that
A9: for Q being Loop of x1 holds f1.Class(EqRel(T,x1),Q) = Class(
EqRel(T,x0),P+Q+-P) and
A10: for Q being Loop of x1 holds f2.Class(EqRel(T,x1),Q) = Class(
EqRel(T,x0),P+Q+-P);
for x being Element of pi_1(T,x1) holds f1.x = f2.x
proof
let x be Element of pi_1(T,x1);
consider L being Loop of x1 such that
A11: x = Class(EqRel(T,x1),L) by Th47;
thus f1.x = Class(EqRel(T,x0),P+L+-P) by A9,A11
.= f2.x by A10,A11;
end;
hence thesis;
end;
end;
reserve x0, x1 for Point of X,
P, Q for Path of x0,x1,
y0, y1 for Point of T,
R, V for Path of y0,y1;
theorem Th48:
x0,x1 are_connected & P,Q are_homotopic implies pi_1-iso(P) = pi_1-iso(Q)
proof
assume that
A1: x0,x1 are_connected and
A2: P,Q are_homotopic;
for x being Element of pi_1(X,x1) holds (pi_1-iso(P)).x = (pi_1-iso(Q)). x
proof
A3: -P, -Q are_homotopic by A1,A2,BORSUK_6:77;
let x be Element of pi_1(X,x1);
consider L being Loop of x1 such that
A4: x = Class(EqRel(X,x1),L) by Th47;
L, L are_homotopic by BORSUK_2:12;
then P+L, Q+L are_homotopic by A1,A2,BORSUK_6:75;
then
A5: P+L+-P, Q+L+-Q are_homotopic by A1,A3,BORSUK_6:75;
thus (pi_1-iso(P)).x = Class(EqRel(X,x0),P+L+-P) by A1,A4,Def6
.= Class(EqRel(X,x0),Q+L+-Q) by A5,Th46
.= (pi_1-iso(Q)).x by A1,A4,Def6;
end;
hence thesis;
end;
theorem
R,V are_homotopic implies pi_1-iso(R) = pi_1-iso(V)
by Th48,BORSUK_2:def 3;
theorem Th50:
x0,x1 are_connected implies pi_1-iso(P) is Homomorphism of pi_1(
X,x1), pi_1(X,x0)
proof
set f = pi_1-iso(P);
assume
A1: x0,x1 are_connected;
now
let x, y be Element of pi_1(X,x1);
consider A being Loop of x1 such that
A2: x = Class(EqRel(X,x1),A) by Th47;
consider B being Loop of x1 such that
A3: y = Class(EqRel(X,x1),B) by Th47;
consider D being Loop of x0 such that
A4: f.y = Class(EqRel(X,x0),D) by Th47;
f.y = Class(EqRel(X,x0),P+B+-P) by A1,A3,Def6;
then
A5: D,P+B+-P are_homotopic by A4,Th46;
A6: P+(A+B)+-P,P+A+-P+(P+B+-P) are_homotopic by A1,Th43;
consider C being Loop of x0 such that
A7: f.x = Class(EqRel(X,x0),C) by Th47;
f.x = Class(EqRel(X,x0),P+A+-P) by A1,A2,Def6;
then C,P+A+-P are_homotopic by A7,Th46;
then C+D,P+A+-P+(P+B+-P) are_homotopic by A5,BORSUK_6:75;
then
A8: P+(A+B)+-P,C+D are_homotopic by A6,BORSUK_6:79;
thus f.(x*y) = f.Class(EqRel(X,x1),A+B) by A2,A3,Lm4
.= Class(EqRel(X,x0),P+(A+B)+-P) by A1,Def6
.= Class(EqRel(X,x0),C+D) by A8,Th46
.= f.x * f.y by A7,A4,Lm4;
end;
hence thesis by GROUP_6:def 6;
end;
registration
let T be non empty pathwise_connected TopSpace, x0, x1 be Point of T,
P be Path of x0,x1;
cluster pi_1-iso(P) -> multiplicative;
coherence
by Th50,BORSUK_2:def 3;
end;
theorem Th51:
x0,x1 are_connected implies pi_1-iso(P) is one-to-one
proof
assume
A1: x0,x1 are_connected;
set f = pi_1-iso(P);
let a, b be object such that
A2: a in dom f and
A3: b in dom f and
A4: f.a = f.b;
consider B being Loop of x1 such that
A5: b = Class(EqRel(X,x1),B) by A3,Th47;
A6: f.b = Class(EqRel(X,x0),P+B+-P) by A1,A5,Def6;
consider A being Loop of x1 such that
A7: a = Class(EqRel(X,x1),A) by A2,Th47;
f.a = Class(EqRel(X,x0),P+A+-P) by A1,A7,Def6;
then P+A+-P, P+B+-P are_homotopic by A4,A6,Th46;
then P+A, P+B are_homotopic by A1,Th27;
then A,B are_homotopic by A1,Th29;
hence thesis by A7,A5,Th46;
end;
theorem Th52:
x0,x1 are_connected implies pi_1-iso(P) is onto
proof
assume
A1: x0,x1 are_connected;
set f = pi_1-iso(P);
thus rng f c= the carrier of pi_1(X,x0);
let y be object;
assume y in the carrier of pi_1(X,x0);
then consider Y being Loop of x0 such that
A2: y = Class(EqRel(X,x0),Y) by Th47;
A3: P+(-P+Y+P)+-P, Y are_homotopic by A1,Th41;
set Z = Class(EqRel(X,x1),-P+Y+P);
dom f = the carrier of pi_1(X,x1) by FUNCT_2:def 1;
then
A4: Z in dom f by Th47;
f.Z = Class(EqRel(X,x0),P+(-P+Y+P)+-P) by A1,Def6
.= y by A2,A3,Th46;
hence thesis by A4,FUNCT_1:def 3;
end;
registration
let T be non empty pathwise_connected TopSpace,
x0, x1 be Point of T, P be Path of x0,x1;
cluster pi_1-iso(P) -> one-to-one onto;
coherence
by Th51,Th52,BORSUK_2:def 3;
end;
theorem Th53:
x0,x1 are_connected implies (pi_1-iso(P))" = pi_1-iso(-P)
proof
set f = pi_1-iso(P);
set g = pi_1-iso(-P);
assume
A1: x0,x1 are_connected;
then f is one-to-one onto by Th51,Th52;
then
A2: f" = (f qua Function)" by TOPS_2:def 4;
A3: f is one-to-one by A1,Th51;
for x being Element of pi_1(X,x0) holds f".x = g.x
proof
let x be Element of pi_1(X,x0);
consider Q being Loop of x0 such that
A4: x = Class(EqRel(X,x0),Q) by Th47;
--P = P by A1,BORSUK_6:43;
then
A5: P+(-P+Q+--P)+-P, Q are_homotopic by A1,Th41;
dom f = the carrier of pi_1(X,x1) by FUNCT_2:def 1;
then
A6: Class(EqRel(X,x1),-P+Q+--P) in dom f by Th47;
f.Class(EqRel(X,x1),-P+Q+--P) = Class(EqRel(X,x0),P+(-P+Q+--P)+-P) by A1
,Def6
.= x by A4,A5,Th46;
hence f".x = Class(EqRel(X,x1),-P+Q+--P) by A3,A2,A6,FUNCT_1:32
.= g.x by A1,A4,Def6;
end;
hence thesis;
end;
theorem
(pi_1-iso(R))" = pi_1-iso(-R)
by Th53,BORSUK_2:def 3;
theorem Th55:
x0,x1 are_connected implies for h being Homomorphism of pi_1(X,
x1), pi_1(X,x0) st h = pi_1-iso(P) holds h is bijective
by Th51,Th52;
theorem
pi_1-iso(R) is bijective;
theorem
x0,x1 are_connected implies pi_1(X,x0), pi_1(X,x1) are_isomorphic
proof
set P = the Path of x1,x0;
assume
A1: x0,x1 are_connected;
then reconsider
h = pi_1-iso(P) as Homomorphism of pi_1(X,x0), pi_1(X,x1) by Th50;
take h;
thus thesis by A1,Th55;
end;
theorem
pi_1(T,y0), pi_1(T,y1) are_isomorphic
proof
set R = the Path of y1,y0;
take pi_1-iso(R);
thus thesis;
end;
begin :: TOP-REAL n
definition
let n be Nat, P, Q be Function of I[01], TOP-REAL n;
func RealHomotopy(P,Q) -> Function of [:I[01],I[01]:], TOP-REAL n means
:
Def7: for s, t being Element of I[01] holds it.(s,t) = (1-t) * P.s + t * Q.s;
existence
proof
set I = the carrier of I[01];
deffunc F(Element of I, Element of I) = (1-$2) * P.$1 + $2 * Q.$1;
consider F being Function of [:I,I:],the carrier of TOP-REAL n such that
A1: for x, y being Element of I holds F.(x,y) = F(x,y) from BINOP_1:
sch 4;
the carrier of [:I[01],I[01]:] = [:I,I:] by BORSUK_1:def 2;
then reconsider F as Function of [:I[01],I[01]:], TOP-REAL n;
take F;
let x, y be Element of I;
thus thesis by A1;
end;
uniqueness
proof
set I = the carrier of I[01];
let f, g be Function of [:I[01],I[01]:], TOP-REAL n such that
A2: for s, t being Element of I[01] holds f.(s,t) = (1-t) * P.s + t * Q.s and
A3: for s, t being Element of I[01] holds g.(s,t) = (1-t) * P.s + t * Q.s;
A4: 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 A2
.= g.(s,t) by A3;
end;
the carrier of [:I[01],I[01]:] = [:I,I:] by BORSUK_1:def 2;
hence f = g by A4,BINOP_1:2;
end;
end;
Lm5: for P, Q being continuous Function of I[01],TOP-REAL n holds RealHomotopy
(P,Q) is continuous
proof
set I = the carrier of I[01];
let P, Q be continuous Function of I[01],TOP-REAL n;
set F = RealHomotopy(P,Q);
set T = the carrier of TOP-REAL n;
set PI = [:P,id I[01]:];
set QI = [:Q,id I[01]:];
deffunc Fb(Element of TOP-REAL n,Element of I) = $2*$1;
deffunc Fa(Element of TOP-REAL n,Element of I) = (1-$2)*$1;
consider Pa being Function of [:T,I:],T such that
A1: for x being Element of T, i being Element of I holds Pa.(x,i) = Fa(x
,i) from BINOP_1:sch 4;
consider Pb being Function of [:T,I:],T such that
A2: for x being Element of T, 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]:] = [:T,I:] by BORSUK_1:def 2;
then reconsider Pa, Pb as Function of [:TOP-REAL n,I[01]:],TOP-REAL n;
A3: Pb is continuous by A2,Th18;
A4: for p being Point of [:I[01],I[01]:] holds F.p = (Pa*PI).p + (Pb*QI).p
proof
A5: dom Q = I by FUNCT_2:def 1;
A6: 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
A7: p = [s,t] by BORSUK_1:10;
A8: dom id I[01] = I & (id I[01]).t = t by FUNCT_1:18,FUNCT_2:def 1;
A9: (Pb*QI).p = Pb.(QI.(s,t)) by A7,FUNCT_2:15
.= Pb.(Q.s,t) by A5,A8,FUNCT_3:def 8
.= t * Q.s by A2;
A10: (Pa*PI).p = Pa.(PI.(s,t)) by A7,FUNCT_2:15
.= Pa.(P.s,t) by A6,A8,FUNCT_3:def 8
.= (1-t) * P.s by A1;
thus F.p = F.(s,t) by A7
.= (Pa*PI).p + (Pb*QI).p by A10,A9,Def7;
end;
Pa is continuous by A1,Th17;
hence thesis by A3,A4,Lm1;
end;
Lm6: for a, b being Point of TOP-REAL n, P, Q being Path of a,b holds for s
being Point of I[01] holds RealHomotopy(P,Q).(s,0) = P.s & RealHomotopy(P,Q).(s
,1) = Q.s & for t being Point of I[01] holds RealHomotopy(P,Q).(0,t) = a &
RealHomotopy(P,Q).(1,t) = b
proof
let a, b be Point of TOP-REAL n, P, Q be Path of a,b;
set F = RealHomotopy(P,Q);
let s be Point of I[01];
thus F.(s,0) = (1-0) * P.s + 0 * Q.s by Def7,BORSUK_1:def 14
.= P.s + 0 * Q.s by RLVECT_1:def 8
.= P.s + 0.TOP-REAL n by RLVECT_1:10
.= P.s by RLVECT_1:4;
thus F.(s,1) = (1-1) * P.s + 1 * Q.s by Def7,BORSUK_1:def 15
.= 0.TOP-REAL n + 1 * Q.s by RLVECT_1:10
.= 0.TOP-REAL n + Q.s by RLVECT_1:def 8
.= Q.s by RLVECT_1:4;
let t be Point of I[01];
A1: P.0[01] = a & Q.0[01] = a by BORSUK_2:def 4;
thus F.(0,t) = (1-t) * P.0[01] + t * Q.0[01] by Def7
.= 1*a - t*a + t*a by A1,RLVECT_1:35
.= 1*a by RLVECT_4:1
.= a by RLVECT_1:def 8;
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 Def7
.= 1*b - t*b + t*b by A2,RLVECT_1:35
.= 1*b by RLVECT_4:1
.= b by RLVECT_1:def 8;
end;
theorem Th59:
for a, b being Point of TOP-REAL n, P, Q being Path of a,b holds
P, Q are_homotopic
proof
let a, b be Point of TOP-REAL n, P, Q be Path of a,b;
take F = RealHomotopy(P,Q);
thus F is continuous by Lm5;
thus thesis by Lm6;
end;
registration
let n be Nat, a, b be Point of TOP-REAL n, 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 Th59;
hence thesis by BORSUK_6:def 11;
end;
end;
theorem Th60:
for a being Point of TOP-REAL n, C being Loop of a holds the
carrier of pi_1(TOP-REAL n,a) = { Class(EqRel(TOP-REAL n,a),C) }
proof
let a be Point of TOP-REAL n, C be Loop of a;
set X = TOP-REAL n;
set E = EqRel(X,a);
hereby
let x be object;
assume x in the carrier of pi_1(X,a);
then consider P being Loop of a such that
A1: x = Class(E,P) by Th47;
P,C are_homotopic by Th59;
then x = Class(E,C) by A1,Th46;
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 Def1;
then x in Class E by A2,EQREL_1:def 3;
hence thesis by Def5;
end;
registration
let n be Nat;
let a be Point of TOP-REAL n;
cluster pi_1(TOP-REAL n,a) -> trivial;
coherence
proof
set C = the constant Loop of a;
set X = TOP-REAL n;
set E = EqRel(X,a);
the carrier of pi_1(X,a) = Class E by Def5;
then { Class(E,C) } = Class E by Th60;
hence thesis by Def5;
end;
end;
theorem
for S being non empty TopSpace, s being Point of S for x, y being
Element of pi_1(S,s) for P, Q being Loop of s st x = Class(EqRel(S,s),P) & y =
Class(EqRel(S,s),Q) holds x*y = Class(EqRel(S,s),P+Q) by Lm4;
:: Added, AK 5.02.2007
theorem Th62:
for C being constant Loop of a holds 1_pi_1(X,a) = Class(EqRel(X ,a),C)
proof
let C be constant Loop of a;
set G = pi_1(X,a);
reconsider g = Class(EqRel(X,a),C) as Element of G by Th47;
set E = EqRel(X,a);
now
let h be Element of G;
consider P being Loop of a such that
A1: h = Class(E,P) by Th47;
A2: P,P+C are_homotopic by BORSUK_6:80;
thus h * g = Class(E,P+C) by A1,Lm4
.= h by A1,A2,Th46;
A3: P,C+P are_homotopic by BORSUK_6:82;
thus g * h = Class(E,C+P) by A1,Lm4
.= h by A1,A3,Th46;
end;
hence thesis by GROUP_1:4;
end;
theorem
for x, y being Element of pi_1(X,a), P being Loop of a st x = Class(
EqRel(X,a),P) & y = Class(EqRel(X,a),-P) holds x" = y
proof
set E = EqRel(X,a);
set G = pi_1(X,a);
let x, y be Element of G, P be Loop of a such that
A1: x = Class(E,P) & y = Class(E,-P);
set C = the constant Loop of a;
A2: -P+P,C are_homotopic by BORSUK_6:86;
A3: y * x = Class(E,-P+P) by A1,Lm4
.= Class(E,C) by A2,Th46
.= 1_G by Th62;
A4: P+-P,C are_homotopic by BORSUK_6:84;
x * y = Class(E,P+-P) by A1,Lm4
.= Class(E,C) by A4,Th46
.= 1_G by Th62;
hence thesis by A3,GROUP_1:def 5;
end;
registration
let n;
let P, Q be continuous Function of I[01],TOP-REAL n;
cluster RealHomotopy(P,Q) -> continuous;
coherence by Lm5;
end;
theorem
for a, b be Point of TOP-REAL n, P, Q be Path of a,b holds
RealHomotopy(P,Q) is Homotopy of P,Q
proof
let a, b be Point of TOP-REAL n, P, Q be Path of a,b;
thus P, Q are_homotopic by Th59;
thus RealHomotopy(P,Q) is continuous;
thus thesis by Lm6;
end;
theorem
a,b are_connected implies EqRel(X,a,b) is non empty total symmetric
transitive by Lm3;