:: Algebraic Properties of Homotopies
:: by Adam Grabowski and Artur Korni{\l}owicz
::
:: 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, XBOOLE_0, FUNCT_1, RELAT_1, SUBSET_1, STRUCT_0,
ZFMISC_1, BORSUK_1, XXREAL_1, CARD_1, XREAL_0, XXREAL_0, ARYTM_1,
ARYTM_3, TOPMETR, PRE_TOPC, GRAPH_1, RCOMP_1, TARSKI, EUCLID, MCART_1,
JGRAPH_2, FUNCT_2, MEMBERED, REAL_1, FINSEQ_1, FINSEQ_2, TOPS_2, TREAL_1,
VALUED_1, ORDINAL2, BORSUK_2, FUNCOP_1, FUNCT_4, BORSUK_6;
notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, XFAMILY, SUBSET_1, ORDINAL1,
NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, REAL_1, MEMBERED, MCART_1,
FINSEQ_1, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_3, FUNCT_2,
FINSEQ_2, STRUCT_0, PRE_TOPC, EUCLID, TOPS_2, RCOMP_1, COMPTS_1,
JGRAPH_2, TREAL_1, FUNCT_4, BORSUK_1, TOPMETR, BINOP_1, BORSUK_2;
constructors REAL_1, RCOMP_1, FINSEQ_4, CONNSP_1, TOPS_2, COMPTS_1, GRCAT_1,
T_0TOPSP, MONOID_0, TREAL_1, BORSUK_2, JGRAPH_2, FUNCOP_1, COMPLEX1,
PCOMPS_1, XTUPLE_0, FUNCT_4, XFAMILY;
registrations XBOOLE_0, RELSET_1, FUNCT_2, NUMBERS, XXREAL_0, XREAL_0,
MEMBERED, STRUCT_0, PRE_TOPC, BORSUK_1, MONOID_0, EUCLID, TOPMETR,
BORSUK_2, BORSUK_3, JGRAPH_2, TOPS_1, COMPTS_1, SUBSET_1, ZFMISC_1,
RELAT_1, XTUPLE_0, ORDINAL1;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions XBOOLE_0, BORSUK_2, TARSKI;
equalities BINOP_1, EUCLID, STRUCT_0, TARSKI;
expansions XBOOLE_0, BORSUK_2, TARSKI;
theorems BORSUK_1, FUNCOP_1, TOPS_2, TREAL_1, FUNCT_2, FUNCT_1, PRE_TOPC,
RCOMP_1, TARSKI, RELAT_1, TOPMETR, FUNCT_4, MCART_1, ZFMISC_1, FUNCT_3,
XBOOLE_0, XBOOLE_1, XCMPLX_1, BORSUK_2, BORSUK_3, BORSUK_4, XREAL_0,
YELLOW12, JORDAN6, JGRAPH_2, TSEP_1, JGRAPH_1, JORDAN5B, MEMBERED,
TOPREAL6, EUCLID, FINSEQ_1, JORDAN1K, XREAL_1, XXREAL_0, FINSEQ_2,
XXREAL_1, XTUPLE_0;
schemes RECDEF_2, DOMAIN_1, XBOOLE_0, JGRAPH_2, PARTFUN1, BINOP_1;
begin :: Preliminaries
scheme
ExFunc3CondD { C() -> non empty set, P,Q,R[set], F,G,H(set) -> set }: ex f
being Function st dom f = C() & for c being Element of C() holds (P[c] implies
f.c = F(c)) & (Q[c] implies f.c = G(c)) & (R[c] implies f.c = H(c))
provided
A1: for c being Element of C() holds (P[c] implies not Q[c]) & (P[c]
implies not R[c]) & (Q[c] implies not R[c]) and
A2: for c being Element of C() holds P[c] or Q[c] or R[c]
proof
A3: for c being set st c in C() holds P[c] or Q[c] or R[c] by A2;
A4: for c being set st c in C() holds (P[c] implies not Q[c]) & (P[c]
implies not R[c]) & (Q[c] implies not R[c]) by A1;
ex f being Function st dom f = C() & for c being set st c in C() holds (
P[c] implies f.c = F(c)) & (Q[c] implies f.c = G(c)) & (R[c] implies f.c = H(c)
) from RECDEF_2:sch 1(A4,A3);
then consider f being Function such that
A5: dom f = C() and
A6: for c being set st c in C() holds (P[c] implies f.c = F(c)) & (Q[c]
implies f.c = G(c)) & (R[c] implies f.c = H(c));
take f;
thus dom f = C() by A5;
let c be Element of C();
thus thesis by A6;
end;
theorem Th1:
the carrier of [:I[01],I[01]:] = [:[.0,1.], [.0,1.]:] by BORSUK_1:40,def 2;
theorem Th2:
for a, b, x being Real st a <= x & x <= b holds (x - a) /
(b - a) in the carrier of Closed-Interval-TSpace (0,1)
proof
let a, b, x be Real;
assume that
A1: a <= x and
A2: x <= b;
A3: a <= b by A1,A2,XXREAL_0:2;
A4: x - a <= b - a by A2,XREAL_1:9;
A5: (x - a) / (b - a) <= 1
proof
per cases by A3,XREAL_1:48;
suppose
b - a = 0;
hence thesis by XCMPLX_1:49;
end;
suppose
b - a > 0;
hence thesis by A4,XREAL_1:185;
end;
end;
A6: x - a >= 0 by A1,XREAL_1:48;
b - a >= 0 by A3,XREAL_1:48;
then (x - a) / (b - a) in [.0,1.] by A5,A6,XXREAL_1:1;
hence thesis by TOPMETR:18;
end;
theorem Th3:
for x being Point of I[01] st x <= 1/2 holds 2 * x is Point of I[01]
proof
let x be Point of I[01];
assume x <= 1/2;
then
A1: 2 * x <= 2 * (1/2) by XREAL_1:64;
0 <= x by BORSUK_1:43;
hence thesis by A1,BORSUK_1:43;
end;
theorem Th4:
for x being Point of I[01] st x >= 1/2 holds 2 * x - 1 is Point of I[01]
proof
let x be Point of I[01];
x <= 1 by BORSUK_1:43;
then 2 * x <= 2 * 1 by XREAL_1:64;
then
A1: 2 * x - 1 <= 2 - 1 by XREAL_1:9;
assume x >= 1/2;
then 2 * x >= 2 * (1/2) by XREAL_1:64;
then 2 * x - 1 >= 1 - 1 by XREAL_1:9;
hence thesis by A1,BORSUK_1:43;
end;
theorem Th5:
for p, q being Point of I[01] holds p * q is Point of I[01]
proof
let p, q be Point of I[01];
A1: 0 <= p by BORSUK_1:43;
p <= 1 & q <= 1 by BORSUK_1:43;
then 0 <= q & p * q <= 1 by A1,BORSUK_1:43,XREAL_1:160;
hence thesis by A1,BORSUK_1:43;
end;
theorem Th6:
for x being Point of I[01] holds 1/2 * x is Point of I[01]
proof
let x be Point of I[01];
x <= 1 by BORSUK_1:43;
then 1/2 * x <= 1/2 * 1 by XREAL_1:64;
then x >= 0 & 1/2 * x <= 1 by BORSUK_1:43,XXREAL_0:2;
hence thesis by BORSUK_1:43;
end;
theorem Th7:
for x being Point of I[01] st x >= 1/2 holds x - 1/4 is Point of I[01]
proof
let x be Point of I[01];
x <= 1 by BORSUK_1:43;
then x <= 1 + 1/4 by XXREAL_0:2;
then
A1: x - 1/4 <= 1 by XREAL_1:20;
assume x >= 1/2;
then x >= 1/4 + 0 by XXREAL_0:2;
then x - 1/4 >= 0 by XREAL_1:19;
hence thesis by A1,BORSUK_1:43;
end;
theorem Th8:
id I[01] is Path of 0[01], 1[01]
proof
set f = id I[01];
f.0 = 0[01] & f.1 = 1[01] by BORSUK_1:def 14,def 15,FUNCT_1:18;
hence thesis by BORSUK_2:def 4;
end;
theorem Th9:
for a, b, c, d being Point of I[01] st a <= b & c <= d holds [:
[.a,b.], [.c,d.]:] is compact non empty Subset of [:I[01], I[01]:]
proof
let a, b, c, d be Point of I[01];
[.a,b.] is Subset of I[01] & [.c,d.] is Subset of I[01] by BORSUK_4:18;
then
A1: [:[.a,b.], [.c,d.]:] c= [:the carrier of I[01], the carrier of I[01]:]
by ZFMISC_1:96;
assume
A2: a <= b & c <= d;
then a in [.a,b.] & c in [.c,d.] by XXREAL_1:1;
then reconsider
Ewa = [:[.a,b.], [.c,d.]:] as non empty Subset of [:I[01], I[01]
:] by A1,BORSUK_1:def 2;
[.a,b.] is compact Subset of I[01] & [.c,d.] is compact Subset of I[01]
by A2,BORSUK_4:24;
then Ewa is compact Subset of [:I[01], I[01]:] by BORSUK_3:23;
hence thesis;
end;
begin :: Affine Maps
theorem Th10:
for S, T being Subset of TOP-REAL 2 st S = {p where p is Point
of TOP-REAL 2 : p`2 <= 2 * p`1 - 1 } & T = {p where p is Point of TOP-REAL 2 :
p`2 <= p`1 } holds AffineMap (1, 0, 1/2, 1/2) .: S = T
proof
set f = AffineMap (1,0,1/2,1/2);
set A = 1, B = 0, C = 1/2, D = 1/2;
let S, T be Subset of TOP-REAL 2;
assume that
A1: S = {p where p is Point of TOP-REAL 2 : p`2 <= 2 * p`1 - 1 } and
A2: T = {p where p is Point of TOP-REAL 2 : p`2 <= p`1 };
f .: S = T
proof
thus f .: S c= T
proof
let x be object;
assume x in f .: S;
then consider y being object such that
y in dom f and
A3: y in S and
A4: x = f.y by FUNCT_1:def 6;
consider p being Point of TOP-REAL 2 such that
A5: y = p and
A6: p`2 <= 2 * p`1 - 1 by A1,A3;
set b = f.p;
f.p = |[A*(p`1)+B,C*(p`2)+D]| by JGRAPH_2:def 2;
then
A7: b`1 = A * (p`1) + B & b`2 = C * (p`2) + D by EUCLID:52;
C * p`2 <= C * (2 * p`1 - 1) by A6,XREAL_1:64;
then C * p`2 + D <= p`1 - C + D by XREAL_1:6;
hence thesis by A2,A4,A5,A7;
end;
let x be object;
assume
A8: x in T;
then
A9: ex p being Point of TOP-REAL 2 st x = p & p`2 <= p`1 by A2;
f is onto by JORDAN1K:36;
then rng f = the carrier of TOP-REAL 2 by FUNCT_2:def 3;
then consider y being object such that
A10: y in dom f and
A11: x = f.y by A8,FUNCT_1:def 3;
reconsider y as Point of TOP-REAL 2 by A10;
set b = f.y;
A12: f.y = |[A*(y`1)+B,C*(y`2)+D]| by JGRAPH_2:def 2;
then b`1 = y`1 by EUCLID:52;
then 2 * b`2 <= 2 * y`1 by A9,A11,XREAL_1:64;
then
A13: 2 * b`2 - 1 <= 2 * y`1 - 1 by XREAL_1:9;
b`2 = C * (y`2) + D by A12,EUCLID:52;
then y in S by A1,A13;
hence thesis by A10,A11,FUNCT_1:def 6;
end;
hence thesis;
end;
theorem Th11:
for S, T being Subset of TOP-REAL 2 st S = {p where p is Point
of TOP-REAL 2 : p`2 >= 2 * p`1 - 1 } & T = {p where p is Point of TOP-REAL 2 :
p`2 >= p`1 } holds AffineMap (1, 0, 1/2, 1/2) .: S = T
proof
set f = AffineMap (1,0,1/2,1/2);
set A = 1, B = 0, C = 1/2, D = 1/2;
let S, T be Subset of TOP-REAL 2;
assume that
A1: S = {p where p is Point of TOP-REAL 2 : p`2 >= 2 * p`1 - 1 } and
A2: T = {p where p is Point of TOP-REAL 2 : p`2 >= p`1 };
f .: S = T
proof
thus f .: S c= T
proof
let x be object;
assume x in f .: S;
then consider y being object such that
y in dom f and
A3: y in S and
A4: x = f.y by FUNCT_1:def 6;
consider p being Point of TOP-REAL 2 such that
A5: y = p and
A6: p`2 >= 2 * p`1 - 1 by A1,A3;
A7: C * p`2 >= C * (2 * p`1 - 1) by A6,XREAL_1:64;
set b = f.p;
A8: f.p = |[A*(p`1)+B,C*(p`2)+D]| by JGRAPH_2:def 2;
then
A9: b`1 = A * (p`1) + B by EUCLID:52;
b`2 = C * (p`2) + D by A8,EUCLID:52;
then b`2 >= p`1 - C + D by A7,XREAL_1:6;
hence thesis by A2,A4,A5,A9;
end;
let x be object;
assume
A10: x in T;
then
A11: ex p being Point of TOP-REAL 2 st x = p & p`2 >= p`1 by A2;
f is onto by JORDAN1K:36;
then rng f = the carrier of TOP-REAL 2 by FUNCT_2:def 3;
then consider y being object such that
A12: y in dom f and
A13: x = f.y by A10,FUNCT_1:def 3;
reconsider y as Point of TOP-REAL 2 by A12;
set b = f.y;
A14: f.y = |[A*(y`1)+B,C*(y`2)+D]| by JGRAPH_2:def 2;
then b`1 = y`1 by EUCLID:52;
then 2 * b`2 >= 2 * y`1 by A11,A13,XREAL_1:64;
then
A15: 2 * b`2 - 1 >= 2 * y`1 - 1 by XREAL_1:9;
b`2 = C * (y`2) + D by A14,EUCLID:52;
then y in S by A1,A15;
hence thesis by A12,A13,FUNCT_1:def 6;
end;
hence thesis;
end;
theorem Th12:
for S, T being Subset of TOP-REAL 2 st S = {p where p is Point
of TOP-REAL 2 : p`2 >= 1 - 2 * p`1 } & T = {p where p is Point of TOP-REAL 2 :
p`2 >= - p`1 } holds AffineMap (1, 0, 1/2, -1/2) .: S = T
proof
set f = AffineMap (1,0,1/2,-1/2);
set A = 1, B = 0, C = 1/2, D = -1/2;
let S, T be Subset of TOP-REAL 2;
assume that
A1: S = {p where p is Point of TOP-REAL 2 : p`2 >= 1 - 2 * p`1 } and
A2: T = {p where p is Point of TOP-REAL 2 : p`2 >= - p`1 };
f .: S = T
proof
thus f .: S c= T
proof
let x be object;
assume x in f .: S;
then consider y being object such that
y in dom f and
A3: y in S and
A4: x = f.y by FUNCT_1:def 6;
consider p being Point of TOP-REAL 2 such that
A5: y = p and
A6: p`2 >= 1 - 2 * p`1 by A1,A3;
set b = f.p;
C * p`2 >= C * (1 - 2 * p`1) by A6,XREAL_1:64;
then
A7: C * p`2 + D >= C - p`1 + D by XREAL_1:6;
A8: f.p = |[A*(p`1)+B,C*(p`2)+D]| by JGRAPH_2:def 2;
then b`1 = A * (p`1) + B by EUCLID:52;
then b`2 >= - b`1 by A8,A7,EUCLID:52;
hence thesis by A2,A4,A5;
end;
let x be object;
assume
A9: x in T;
then
A10: ex p being Point of TOP-REAL 2 st x = p & p`2 >= - p`1 by A2;
f is onto by JORDAN1K:36;
then rng f = the carrier of TOP-REAL 2 by FUNCT_2:def 3;
then consider y being object such that
A11: y in dom f and
A12: x = f.y by A9,FUNCT_1:def 3;
reconsider y as Point of TOP-REAL 2 by A11;
set b = f.y;
A13: f.y = |[A*(y`1)+B,C*(y`2)+D]| by JGRAPH_2:def 2;
then b`1 = y`1 by EUCLID:52;
then 2 * b`2 >= 2 * (- y`1) by A10,A12,XREAL_1:64;
then
A14: 2 * b`2 + 1 >= 2 * (- y`1) + 1 by XREAL_1:6;
b`2 = C * (y`2) + D by A13,EUCLID:52;
then y`2 >= 1 - 2 * y`1 by A14;
then y in S by A1;
hence thesis by A11,A12,FUNCT_1:def 6;
end;
hence thesis;
end;
theorem Th13:
for S, T being Subset of TOP-REAL 2 st S = {p where p is Point
of TOP-REAL 2 : p`2 <= 1 - 2 * p`1 } & T = {p where p is Point of TOP-REAL 2 :
p`2 <= - p`1 } holds AffineMap (1, 0, 1/2, -1/2) .: S = T
proof
set f = AffineMap (1,0,1/2,-1/2);
set A = 1, B = 0, C = 1/2, D = -1/2;
let S, T be Subset of TOP-REAL 2;
assume that
A1: S = {p where p is Point of TOP-REAL 2 : p`2 <= 1 - 2 * p`1 } and
A2: T = {p where p is Point of TOP-REAL 2 : p`2 <= - p`1 };
f .: S = T
proof
thus f .: S c= T
proof
let x be object;
assume x in f .: S;
then consider y being object such that
y in dom f and
A3: y in S and
A4: x = f.y by FUNCT_1:def 6;
consider p being Point of TOP-REAL 2 such that
A5: y = p and
A6: p`2 <= 1 - 2 * p`1 by A1,A3;
set b = f.p;
C * p`2 <= C * (1 - 2 * p`1) by A6,XREAL_1:64;
then
A7: C * p`2 + D <= C - p`1 + D by XREAL_1:6;
A8: f.p = |[A*(p`1)+B,C*(p`2)+D]| by JGRAPH_2:def 2;
then b`1 = A * (p`1) + B by EUCLID:52;
then b`2 <= - b`1 by A8,A7,EUCLID:52;
hence thesis by A2,A4,A5;
end;
let x be object;
assume
A9: x in T;
then
A10: ex p being Point of TOP-REAL 2 st x = p & p`2 <= - p`1 by A2;
f is onto by JORDAN1K:36;
then rng f = the carrier of TOP-REAL 2 by FUNCT_2:def 3;
then consider y being object such that
A11: y in dom f and
A12: x = f.y by A9,FUNCT_1:def 3;
reconsider y as Point of TOP-REAL 2 by A11;
set b = f.y;
A13: f.y = |[A*(y`1)+B,C*(y`2)+D]| by JGRAPH_2:def 2;
then b`1 = y`1 by EUCLID:52;
then 2 * b`2 <= 2 * (- y`1) by A10,A12,XREAL_1:64;
then
A14: 2 * b`2 + 1 <= 2 * (- y`1) + 1 by XREAL_1:6;
b`2 = C * (y`2) + D by A13,EUCLID:52;
then y`2 <= 1 - 2 * y`1 by A14;
then y in S by A1;
hence thesis by A11,A12,FUNCT_1:def 6;
end;
hence thesis;
end;
begin :: Real-membered Structures
theorem
for T being non empty 1-sorted holds T is real-membered iff for
x being Element of T holds x is real
proof
let T be non empty 1-sorted;
thus T is real-membered implies for x being Element of T holds x is real;
assume for x being Element of T holds x is real;
then for x being object st x in the carrier of T holds x is real;
then the carrier of T is real-membered by MEMBERED:def 3;
hence thesis by TOPMETR:def 8;
end;
registration
cluster non empty real-membered for 1-sorted;
existence
proof
take I[01];
thus thesis;
end;
cluster non empty real-membered for TopSpace;
existence
proof
take I[01];
thus thesis;
end;
end;
registration
let T be real-membered 1-sorted;
cluster -> real for Element of T;
coherence;
end;
registration
let T be real-membered TopStruct;
cluster -> real-membered for SubSpace of T;
coherence;
end;
registration
let S, T be real-membered non empty TopSpace, p be Element of [:S, T:];
cluster p`1 -> real;
coherence
proof
p in the carrier of [:S, T:];
then p in [:the carrier of S, the carrier of T:] by BORSUK_1:def 2;
then p`1 in the carrier of S by MCART_1:10;
hence thesis;
end;
cluster p`2 -> real;
coherence
proof
p in the carrier of [:S, T:];
then p in [:the carrier of S, the carrier of T:] by BORSUK_1:def 2;
then p`2 in the carrier of T by MCART_1:10;
hence thesis;
end;
end;
registration
let T be non empty SubSpace of [:I[01], I[01]:], x be Point of T;
cluster x`1 -> real;
coherence
proof
the carrier of T c= the carrier of [:I[01], I[01]:] & x in the carrier
of T by BORSUK_1:1;
then reconsider x9 = x as Point of [:I[01], I[01]:];
x9`1 is real;
hence thesis;
end;
cluster x`2 -> real;
coherence
proof
the carrier of T c= the carrier of [:I[01], I[01]:] & x in the carrier
of T by BORSUK_1:1;
then reconsider x9 = x as Point of [:I[01], I[01]:];
x9`2 is real;
hence thesis;
end;
end;
begin :: Closed Subsets of TOP-REAL 2
theorem Th15:
{p where p is Point of TOP-REAL 2 : p`2 <= 2 * p`1 - 1 } is
closed Subset of TOP-REAL 2
proof
reconsider L = {p where p is Point of TOP-REAL 2 : p`2 <= p`1 } as closed
Subset of TOP-REAL 2 by JGRAPH_2:46;
set f = AffineMap (1,0,1/2,1/2);
defpred P[Point of TOP-REAL 2] means $1`2 <= 2 * $1`1 - 1;
{p where p is Point of TOP-REAL 2 : P[p] } is Subset of TOP-REAL 2 from
JGRAPH_2:sch 1;
then reconsider
K = {p where p is Point of TOP-REAL 2 : p`2 <= 2 * p`1 - 1 } as
Subset of TOP-REAL 2;
K c= the carrier of TOP-REAL 2;
then
A1: K c= dom f by FUNCT_2:def 1;
A2: f .: K = L by Th10;
f is one-to-one by JGRAPH_2:44;
then K = f " (f .: K) by A1,FUNCT_1:94;
hence thesis by A2,PRE_TOPC:def 6;
end;
theorem Th16:
{p where p is Point of TOP-REAL 2 : p`2 >= 2 * p`1 - 1 } is
closed Subset of TOP-REAL 2
proof
reconsider L = {p where p is Point of TOP-REAL 2 : p`2 >= p`1 } as closed
Subset of TOP-REAL 2 by JGRAPH_2:46;
set f = AffineMap (1,0,1/2,1/2);
defpred P[Point of TOP-REAL 2] means $1`2 >= 2 * $1`1 - 1;
{p where p is Point of TOP-REAL 2 : P[p] } is Subset of TOP-REAL 2 from
JGRAPH_2:sch 1;
then reconsider
K = {p where p is Point of TOP-REAL 2 : p`2 >= 2 * p`1 - 1 } as
Subset of TOP-REAL 2;
K c= the carrier of TOP-REAL 2;
then
A1: K c= dom f by FUNCT_2:def 1;
A2: f .: K = L by Th11;
f is one-to-one by JGRAPH_2:44;
then K = f " (f .: K) by A1,FUNCT_1:94;
hence thesis by A2,PRE_TOPC:def 6;
end;
theorem Th17:
{p where p is Point of TOP-REAL 2 : p`2 <= 1 - 2 * p`1 } is
closed Subset of TOP-REAL 2
proof
reconsider L = {p where p is Point of TOP-REAL 2 : p`2 <= - p`1 } as closed
Subset of TOP-REAL 2 by JGRAPH_2:47;
set f = AffineMap (1,0,1/2,-1/2);
defpred P[Point of TOP-REAL 2] means $1`2 <= 1 - 2 * $1`1;
{p where p is Point of TOP-REAL 2 : P[p] } is Subset of TOP-REAL 2 from
JGRAPH_2:sch 1;
then reconsider
K = {p where p is Point of TOP-REAL 2 : p`2 <= 1 - 2 * p`1 } as
Subset of TOP-REAL 2;
K c= the carrier of TOP-REAL 2;
then
A1: K c= dom f by FUNCT_2:def 1;
A2: f .: K = L by Th13;
f is one-to-one by JGRAPH_2:44;
then K = f " (f .: K) by A1,FUNCT_1:94;
hence thesis by A2,PRE_TOPC:def 6;
end;
theorem Th18:
{p where p is Point of TOP-REAL 2 : p`2 >= 1 - 2 * p`1 } is
closed Subset of TOP-REAL 2
proof
reconsider L = {p where p is Point of TOP-REAL 2 : p`2 >= - p`1 } as closed
Subset of TOP-REAL 2 by JGRAPH_2:47;
set f = AffineMap (1,0,1/2,-1/2);
defpred P[Point of TOP-REAL 2] means $1`2 >= 1 - 2 * $1`1;
{p where p is Point of TOP-REAL 2 : P[p] } is Subset of TOP-REAL 2 from
JGRAPH_2:sch 1;
then reconsider
K = {p where p is Point of TOP-REAL 2 : p`2 >= 1 - 2 * p`1 } as
Subset of TOP-REAL 2;
K c= the carrier of TOP-REAL 2;
then
A1: K c= dom f by FUNCT_2:def 1;
A2: f .: K = L by Th12;
f is one-to-one by JGRAPH_2:44;
then K = f " (f .: K) by A1,FUNCT_1:94;
hence thesis by A2,PRE_TOPC:def 6;
end;
theorem Th19:
{p where p is Point of TOP-REAL 2 : p`2 >= 1 - 2 * p`1 & p`2 >=
2 * p`1 - 1 } is closed Subset of TOP-REAL 2
proof
defpred R[Point of TOP-REAL 2] means $1`2 >= 2 * $1`1 - 1;
reconsider L = { p where p is Point of TOP-REAL 2 : R[p] } as closed Subset
of TOP-REAL 2 by Th16;
defpred P[Point of TOP-REAL 2] means $1`2 >= 1 - 2 * $1`1;
reconsider K = { p where p is Point of TOP-REAL 2 : P[p] } as closed Subset
of TOP-REAL 2 by Th18;
set T = {p where p is Point of TOP-REAL 2 : P[p] & R[p] };
{p where p is Point of TOP-REAL 2 : P[p] & R[p] } = { p where p is Point
of TOP-REAL 2 : P[p] } /\ { p where p is Point of TOP-REAL 2 : R[p] } from
DOMAIN_1:sch 10;
then T = K /\ L;
hence thesis;
end;
theorem Th20:
ex f being Function of [:R^1,R^1:], TOP-REAL 2 st for x, y being
Real holds f. [x,y] = <*x,y*>
proof
defpred P[Element of REAL,Element of REAL,set] means ex c being Element of
REAL 2 st c = $3 & $3 = <*$1,$2*>;
A1: for x, y being Element of REAL ex u being Element of REAL 2 st P[x,y,u]
proof
let x, y be Element of REAL;
take <*x,y*>;
<*x,y*> is Element of REAL 2 by FINSEQ_2:137;
hence thesis;
end;
consider f being Function of [:REAL,REAL:],REAL 2 such that
A2: for x, y being Element of REAL holds P[x,y,f.(x,y)] from BINOP_1:sch
3(A1);
the carrier of [:R^1,R^1:] = [:the carrier of R^1,the carrier of R^1:]
by BORSUK_1:def 2;
then reconsider f as Function of [:R^1,R^1:], TOP-REAL 2 by EUCLID:22
,TOPMETR:17;
take f;
for x, y being Real holds f. [x,y] = <*x,y*>
proof
let x, y be Real;
reconsider x,y as Element of REAL by XREAL_0:def 1;
P[x,y,f.(x,y)] by A2;
hence thesis;
end;
hence thesis;
end;
theorem Th21:
{ p where p is Point of [:R^1,R^1:] : p`2 <= 1 - 2 * (p`1) } is
closed Subset of [:R^1,R^1:]
proof
set GG = [:R^1,R^1:], SS = TOP-REAL 2;
defpred P[Point of GG] means $1`2 <= 1 - 2 * ($1`1);
defpred R[Point of SS] means $1`2 <= 1 - 2 * ($1`1);
reconsider K = { p where p is Point of GG : P[p] } as Subset of GG from
DOMAIN_1:sch 7;
reconsider L = { p where p is Point of SS : R[p] } as Subset of SS from
DOMAIN_1:sch 7;
consider f being Function of GG, SS such that
A1: for x, y being Real holds f. [x,y] = <*x,y*> by Th20;
A2: L c= f .: K
proof
let x be object;
assume x in L;
then consider z being Point of SS such that
A3: z = x and
A4: R[z];
the carrier of SS = REAL 2 by EUCLID:22;
then z is Tuple of 2,REAL by FINSEQ_2:131;
then consider x1, y1 being Element of REAL such that
A5: z = <*x1, y1*> by FINSEQ_2:100;
z`1 = x1 by A5,EUCLID:52;
then
A6: y1 <= 1 - 2 * x1 by A4,A5,EUCLID:52;
set Y = [x1, y1];
A7: Y in [:REAL, REAL:] by ZFMISC_1:87;
then
A8: Y in the carrier of GG by BORSUK_1:def 2,TOPMETR:17;
reconsider Y as Point of GG by A7,BORSUK_1:def 2,TOPMETR:17;
A9: Y in dom f by A8,FUNCT_2:def 1;
Y`1 = x1 & Y`2 = y1;
then
A10: Y in K by A6;
x = f.Y by A1,A3,A5;
hence thesis by A10,A9,FUNCT_1:def 6;
end;
A11: f is being_homeomorphism by A1,TOPREAL6:76;
f .: K c= L
proof
let x be object;
assume x in f .: K;
then consider y being object such that
y in dom f and
A12: y in K and
A13: x = f.y by FUNCT_1:def 6;
consider z being Point of GG such that
A14: z = y and
A15: P[z] by A12;
z in the carrier of GG;
then z in [:the carrier of R^1, the carrier of R^1:] by BORSUK_1:def 2;
then consider x1, y1 being object such that
A16: x1 in the carrier of R^1 & y1 in the carrier of R^1 and
A17: z = [x1, y1] by ZFMISC_1:def 2;
reconsider x1, y1 as Real by A16;
A18: x = |[ x1, y1 ]| by A1,A13,A14,A17;
then reconsider x9 = x as Point of SS;
A19: z`1 = x1 & z`2 = y1 by A17;
x9`1 = x1 & x9`2 = y1 by A18,FINSEQ_1:44;
hence thesis by A15,A19;
end;
then f .: K = L by A2;
hence thesis by A11,Th17,TOPS_2:58;
end;
theorem Th22:
{ p where p is Point of [:R^1,R^1:] : p`2 <= 2 * (p`1) - 1 } is
closed Subset of [:R^1,R^1:]
proof
set GG = [:R^1,R^1:], SS = TOP-REAL 2;
defpred P[Point of GG] means $1`2 <= 2 * ($1`1) - 1;
defpred R[Point of SS] means $1`2 <= 2 * ($1`1) - 1;
reconsider K = { p where p is Point of GG : P[p] } as Subset of GG from
DOMAIN_1:sch 7;
reconsider L = { p where p is Point of SS : R[p] } as Subset of SS from
DOMAIN_1:sch 7;
consider f being Function of GG, SS such that
A1: for x, y being Real holds f. [x,y] = <*x,y*> by Th20;
A2: L c= f .: K
proof
let x be object;
assume x in L;
then consider z being Point of SS such that
A3: z = x and
A4: R[z];
the carrier of SS = REAL 2 by EUCLID:22;
then z is Tuple of 2,REAL by FINSEQ_2:131;
then consider x1, y1 being Element of REAL such that
A5: z = <*x1, y1*> by FINSEQ_2:100;
z`1 = x1 by A5,EUCLID:52;
then
A6: y1 <= 2 * x1 - 1 by A4,A5,EUCLID:52;
set Y = [x1, y1];
A7: Y in [:the carrier of R^1, the carrier of R^1:] by TOPMETR:17,ZFMISC_1:87;
then
A8: Y in the carrier of GG by BORSUK_1:def 2;
reconsider Y as Point of GG by A7,BORSUK_1:def 2;
A9: Y in dom f by A8,FUNCT_2:def 1;
Y`1 = x1 & Y`2 = y1;
then
A10: Y in K by A6;
x = f.Y by A1,A3,A5;
hence thesis by A10,A9,FUNCT_1:def 6;
end;
A11: f is being_homeomorphism by A1,TOPREAL6:76;
f .: K c= L
proof
let x be object;
assume x in f .: K;
then consider y being object such that
y in dom f and
A12: y in K and
A13: x = f.y by FUNCT_1:def 6;
consider z being Point of GG such that
A14: z = y and
A15: P[z] by A12;
z in the carrier of GG;
then z in [:the carrier of R^1, the carrier of R^1:] by BORSUK_1:def 2;
then consider x1, y1 being object such that
A16: x1 in the carrier of R^1 & y1 in the carrier of R^1 and
A17: z = [x1, y1] by ZFMISC_1:def 2;
reconsider x1, y1 as Real by A16;
A18: x = |[ x1, y1 ]| by A1,A13,A14,A17;
then reconsider x9 = x as Point of SS;
A19: z`1 = x1 & z`2 = y1 by A17;
x9`1 = x1 & x9`2 = y1 by A18,FINSEQ_1:44;
hence thesis by A15,A19;
end;
then f .: K = L by A2;
hence thesis by A11,Th15,TOPS_2:58;
end;
theorem Th23:
{ p where p is Point of [:R^1,R^1:] : p`2 >= 1 - 2 * (p`1) & p`2
>= 2 * (p`1) - 1 } is closed Subset of [:R^1,R^1:]
proof
set GG = [:R^1,R^1:], SS = TOP-REAL 2;
defpred P[Point of GG] means $1`2 >= 1 - 2 * ($1`1) & $1`2 >= 2 * ($1`1) - 1;
defpred R[Point of SS] means $1`2 >= 1 - 2 * ($1`1) & $1`2 >= 2 * ($1`1) - 1;
reconsider K = { p where p is Point of GG : P[p] } as Subset of GG from
DOMAIN_1:sch 7;
reconsider L = { p where p is Point of SS : R[p] } as Subset of SS from
DOMAIN_1:sch 7;
consider f being Function of GG, SS such that
A1: for x, y being Real holds f. [x,y] = <*x,y*> by Th20;
A2: L c= f .: K
proof
let x be object;
assume x in L;
then consider z being Point of SS such that
A3: z = x and
A4: R[z];
the carrier of SS = REAL 2 by EUCLID:22;
then z is Tuple of 2,REAL by FINSEQ_2:131;
then consider x1, y1 being Element of REAL such that
A5: z = <*x1, y1*> by FINSEQ_2:100;
z`1 = x1 by A5,EUCLID:52;
then
A6: y1 >= 1 - 2 * x1 & y1 >= 2 * x1 - 1 by A4,A5,EUCLID:52;
set Y = [x1, y1];
A7: Y in [:the carrier of R^1, the carrier of R^1:] by TOPMETR:17,ZFMISC_1:87;
then
A8: Y in the carrier of GG by BORSUK_1:def 2;
reconsider Y as Point of GG by A7,BORSUK_1:def 2;
A9: Y in dom f by A8,FUNCT_2:def 1;
Y`1 = x1 & Y`2 = y1;
then
A10: Y in K by A6;
x = f.Y by A1,A3,A5;
hence thesis by A10,A9,FUNCT_1:def 6;
end;
A11: f is being_homeomorphism by A1,TOPREAL6:76;
f .: K c= L
proof
let x be object;
assume x in f .: K;
then consider y being object such that
y in dom f and
A12: y in K and
A13: x = f.y by FUNCT_1:def 6;
consider z being Point of GG such that
A14: z = y and
A15: P[z] by A12;
z in the carrier of GG;
then z in [:the carrier of R^1, the carrier of R^1:] by BORSUK_1:def 2;
then consider x1, y1 being object such that
A16: x1 in the carrier of R^1 & y1 in the carrier of R^1 and
A17: z = [x1, y1] by ZFMISC_1:def 2;
reconsider x1, y1 as Real by A16;
A18: x = |[ x1, y1 ]| by A1,A13,A14,A17;
then reconsider x9 = x as Point of SS;
A19: z`1 = x1 & z`2 = y1 by A17;
x9`1 = x1 & x9`2 = y1 by A18,FINSEQ_1:44;
hence thesis by A15,A19;
end;
then f .: K = L by A2;
hence thesis by A11,Th19,TOPS_2:58;
end;
theorem Th24:
{ p where p is Point of [:I[01],I[01]:] : p`2 <= 1 - 2 * (p`1) }
is closed non empty Subset of [:I[01],I[01]:]
proof
set GG = [:I[01],I[01]:], SS = [:R^1,R^1:];
0 in the carrier of I[01] by BORSUK_1:43;
then [0,0] in [:the carrier of I[01], the carrier of I[01]:] by ZFMISC_1:87;
then reconsider x = [0,0] as Point of GG by BORSUK_1:def 2;
reconsider PA = { p where p is Point of SS : p`2 <= 1 - 2 * (p`1) } as
closed Subset of SS by Th21;
set P0 = { p where p is Point of GG : p`2 <= 1 - 2 * (p`1) };
A1: GG is SubSpace of SS by BORSUK_3:21;
A2: P0 = PA /\ [#] GG
proof
thus P0 c= PA /\ [#] GG
proof
let x be object;
A3: the carrier of GG c= the carrier of SS by A1,BORSUK_1:1;
assume x in P0;
then
A4: ex p being Point of GG st x = p & p`2 <= 1 - 2 * (p`1);
then x in the carrier of GG;
then reconsider a = x as Point of SS by A3;
a`2 <= 1 - 2 * (a`1) by A4;
then x in PA;
hence thesis by A4,XBOOLE_0:def 4;
end;
let x be object;
assume
A5: x in PA /\ [#] GG;
then x in PA by XBOOLE_0:def 4;
then ex p being Point of SS st x = p & p`2 <= 1 - 2 * (p`1);
hence thesis by A5;
end;
x`2 <= 1 - 2 * (x`1);
then x in P0;
hence thesis by A1,A2,PRE_TOPC:13;
end;
theorem Th25:
{ p where p is Point of [:I[01],I[01]:] : p`2 >= 1 - 2 * (p`1) &
p`2 >= 2 * (p`1) - 1 } is closed non empty Subset of [:I[01],I[01]:]
proof
set GG = [:I[01],I[01]:], SS = [:R^1,R^1:];
1 in the carrier of I[01] by BORSUK_1:43;
then [1,1] in [:the carrier of I[01], the carrier of I[01]:] by ZFMISC_1:87;
then reconsider x = [1,1] as Point of GG by BORSUK_1:def 2;
reconsider PA = { p where p is Point of SS : p`2 >= 1 - 2 * (p`1) & p`2 >= 2
* (p`1) - 1 } as closed Subset of SS by Th23;
set P0 = { p where p is Point of GG : p`2 >= 1 - 2 * (p`1) & p`2 >= 2 * (p`1
) - 1 };
A1: x`2 >= 2 * (x`1) - 1;
A2: GG is SubSpace of SS by BORSUK_3:21;
A3: P0 = PA /\ [#] GG
proof
thus P0 c= PA /\ [#] GG
proof
let x be object;
A4: the carrier of GG c= the carrier of SS by A2,BORSUK_1:1;
assume x in P0;
then
A5: ex p being Point of GG st x = p & p`2 >= 1 - 2 * (p`1) & p`2 >= 2 *
(p`1) - 1;
then x in the carrier of GG;
then reconsider a = x as Point of SS by A4;
a`2 >= 1 - 2 * (a`1) by A5;
then x in PA by A5;
hence thesis by A5,XBOOLE_0:def 4;
end;
let x be object;
assume
A6: x in PA /\ [#] GG;
then x in PA by XBOOLE_0:def 4;
then
ex p being Point of SS st x = p & p`2 >= 1 - 2 * (p`1) & p`2 >= 2 * (
p`1) - 1;
hence thesis by A6;
end;
x`2 >= 1 - 2 * (x`1);
then x in P0 by A1;
hence thesis by A2,A3,PRE_TOPC:13;
end;
theorem Th26:
{ p where p is Point of [:I[01],I[01]:] : p`2 <= 2 * (p`1) - 1 }
is closed non empty Subset of [:I[01],I[01]:]
proof
set GG = [:I[01],I[01]:], SS = [:R^1,R^1:];
0 in the carrier of I[01] & 1 in the carrier of I[01] by BORSUK_1:43;
then [1,0] in [:the carrier of I[01], the carrier of I[01]:] by ZFMISC_1:87;
then reconsider x = [1,0] as Point of GG by BORSUK_1:def 2;
reconsider PA = { p where p is Point of SS : p`2 <= 2 * (p`1) - 1 } as
closed Subset of SS by Th22;
set P0 = { p where p is Point of GG : p`2 <= 2 * (p`1) - 1 };
A1: GG is SubSpace of SS by BORSUK_3:21;
A2: P0 = PA /\ [#] GG
proof
thus P0 c= PA /\ [#] GG
proof
let x be object;
A3: the carrier of GG c= the carrier of SS by A1,BORSUK_1:1;
assume x in P0;
then
A4: ex p being Point of GG st x = p & p`2 <= 2 * (p`1) - 1;
then x in the carrier of GG;
then reconsider a = x as Point of SS by A3;
a`2 <= 2 * (a`1) - 1 by A4;
then x in PA;
hence thesis by A4,XBOOLE_0:def 4;
end;
let x be object;
assume
A5: x in PA /\ [#] GG;
then x in PA by XBOOLE_0:def 4;
then ex p being Point of SS st x = p & p`2 <= 2 * (p`1) - 1;
hence thesis by A5;
end;
x`2 <= 2 * (x`1) - 1;
then x in P0;
hence thesis by A1,A2,PRE_TOPC:13;
end;
theorem Th27:
for S, T being non empty TopSpace, p being Point of [:S, T:]
holds p`1 is Point of S & p`2 is Point of T
proof
let S, T be non empty TopSpace, p be Point of [:S, T:];
p in the carrier of [:S, T:];
then p in [:the carrier of S, the carrier of T:] by BORSUK_1:def 2;
hence thesis by MCART_1:10;
end;
theorem Th28:
for A, B being Subset of [:I[01],I[01]:] st A = [:[.0,1/2.], [.0
,1.]:] & B = [:[.1/2,1.], [.0,1.]:] holds [#] ([:I[01],I[01]:] | A) \/ [#] ([:
I[01],I[01]:] | B) = [#] [:I[01],I[01]:]
proof
let A, B be Subset of [:I[01],I[01]:];
assume
A1: A = [:[.0,1/2.], [.0,1.]:] & B = [:[.1/2,1.], [.0,1.]:];
[#] ([:I[01],I[01]:] | A) \/ [#] ([:I[01],I[01]:] | B) = A \/ [#] ([:
I[01],I[01]:] | B) by PRE_TOPC:def 5
.= A \/ B by PRE_TOPC:def 5
.= [:[.0,1/2.] \/ [.1/2,1.], [.0,1.]:] by A1,ZFMISC_1:97
.= [:[.0,1.], [.0,1.]:] by XXREAL_1:174
.= [#] [:I[01],I[01]:] by BORSUK_1:40,def 2;
hence thesis;
end;
theorem Th29:
for A, B being Subset of [:I[01],I[01]:] st A = [:[.0,1/2.], [.0
,1.]:] & B = [:[.1/2,1.], [.0,1.]:] holds [#] ([:I[01],I[01]:] | A) /\ [#] ([:
I[01],I[01]:] | B) = [:{1/2}, [.0,1.] :]
proof
let A, B be Subset of [:I[01],I[01]:];
assume
A1: A = [:[.0,1/2.], [.0,1.]:] & B = [:[.1/2,1.], [.0,1.]:];
[#] ([:I[01],I[01]:] | A) /\ [#] ([:I[01],I[01]:] | B) = A /\ [#] ([:
I[01],I[01]:] | B) by PRE_TOPC:def 5
.= A /\ B by PRE_TOPC:def 5
.= [:[.0,1/2.] /\ [.1/2,1.], [.0,1.]:] by A1,ZFMISC_1:99
.= [:{1/2}, [.0,1.]:] by XXREAL_1:418;
hence thesis;
end;
begin :: Compact Spaces
registration
let T be TopStruct;
cluster empty compact for Subset of T;
existence
proof
take {}T;
thus thesis;
end;
end;
theorem Th30:
for T being TopStruct holds {} is empty compact Subset of T
proof
let T be TopStruct;
{}T c= the carrier of T;
hence thesis;
end;
theorem Th31:
for T being TopStruct, a, b being Real st a > b holds [.a
,b.] is empty compact Subset of T
proof
let T be TopStruct, a, b be Real;
assume a > b;
then [.a,b.] = {}T by XXREAL_1:29;
hence thesis;
end;
theorem
for a, b, c, d being Point of I[01] holds [:[.a,b.], [.c,d.]:] is
compact Subset of [:I[01], I[01]:]
proof
let a, b, c, d be Point of I[01];
per cases;
suppose
a <= b & c <= d;
hence thesis by Th9;
end;
suppose
a > b & c <= d;
then reconsider A = [.a,b.] as empty Subset of I[01] by Th31;
[:A, [.c,d.]:] = {};
hence thesis by Th30;
end;
suppose
a > b & c > d;
then reconsider A = [.c,d.] as empty Subset of I[01] by Th31;
[:[.a,b.], A:] = {};
hence thesis by Th30;
end;
suppose
a <= b & c > d;
then reconsider A = [.c,d.] as empty Subset of I[01] by Th31;
[:[.a,b.], A:] = {};
hence thesis by Th30;
end;
end;
begin :: Continuous Maps
definition
let a, b, c, d be Real;
func L[01](a,b,c,d) -> Function of Closed-Interval-TSpace(a,b),
Closed-Interval-TSpace(c,d) equals
L[01]((#)(c,d),(c,d)(#)) * P[01](a,b,(#)(0,1
),(0,1)(#));
correctness;
end;
theorem Th33:
for a, b, c, d being Real st a < b & c < d holds L[01](a,
b,c,d).a = c & L[01](a,b,c,d).b = d
proof
let a, b, c, d be Real;
assume that
A1: a < b and
A2: c < d;
a in [.a,b.] by A1,XXREAL_1:1;
then a in the carrier of Closed-Interval-TSpace (a,b) by A1,TOPMETR:18;
then a in dom P[01](a,b,(#)(0,1),(0,1)(#)) by FUNCT_2:def 1;
hence L[01](a,b,c,d).a = L[01]((#)(c,d),(c,d)(#)).(P[01](a,b,(#)(0,1),(0,1)
(#)).a) by FUNCT_1:13
.= L[01]((#)(c,d),(c,d)(#)).(P[01](a,b,(#)(0,1),(0,1)(#)).(#)(a,b)) by A1,
TREAL_1:def 1
.= L[01]((#)(c,d),(c,d)(#)).((#)(0,1)) by A1,TREAL_1:13
.= (#)(c,d) by A2,TREAL_1:9
.= c by A2,TREAL_1:def 1;
b in [.a,b.] by A1,XXREAL_1:1;
then b in the carrier of Closed-Interval-TSpace (a,b) by A1,TOPMETR:18;
then b in dom P[01](a,b,(#)(0,1),(0,1)(#)) by FUNCT_2:def 1;
hence L[01](a,b,c,d).b = L[01]((#)(c,d),(c,d)(#)).(P[01](a,b,(#)(0,1),(0,1)
(#)).b) by FUNCT_1:13
.= L[01]((#)(c,d),(c,d)(#)).(P[01](a,b,(#)(0,1),(0,1)(#)).(a,b)(#)) by A1,
TREAL_1:def 2
.= L[01]((#)(c,d),(c,d)(#)).((0,1)(#)) by A1,TREAL_1:13
.= (c,d)(#) by A2,TREAL_1:9
.= d by A2,TREAL_1:def 2;
end;
theorem Th34:
for a, b, c, d being Real st a < b & c <= d holds L[01](a
,b,c,d) is continuous Function of Closed-Interval-TSpace(a,b),
Closed-Interval-TSpace(c,d)
proof
let a, b, c, d be Real;
assume a < b & c <= d;
then L[01]((#)(c,d),(c,d)(#)) is continuous Function of
Closed-Interval-TSpace(0,1 ),Closed-Interval-TSpace(c,d) & P[01](a,b,(#)(0,1),(
0,1)(#)) is continuous Function of Closed-Interval-TSpace(a,b),
Closed-Interval-TSpace(0,1) by TREAL_1:8,12;
hence thesis;
end;
theorem Th35:
for a, b, c, d being Real st a < b & c <= d for x being
Real st a <= x & x <= b holds L[01](a,b,c,d).x = ((d - c)/(b - a)) * (x
- a) + c
proof
A1: 0 = (#)(0,1) & 1 = (0,1)(#) by TREAL_1:def 1,def 2;
let a, b, c, d be Real;
assume
A2: a < b;
set G = P[01](a,b,(#)(0,1),(0,1)(#));
set F = L[01]((#)(c,d),(c,d)(#));
set f = L[01](a,b,c,d);
assume
A3: c <= d;
then
A4: (#)(c,d) = c & (c,d)(#) = d by TREAL_1:def 1,def 2;
let x be Real;
assume
A5: a <= x;
set X = (x-a)/(b-a);
assume
A6: x <= b;
then
A7: X in the carrier of Closed-Interval-TSpace (0,1) by A5,Th2;
x in [.a,b.] by A5,A6,XXREAL_1:1;
then
A8: x in the carrier of Closed-Interval-TSpace (a,b) by A2,TOPMETR:18;
then x in dom G by FUNCT_2:def 1;
then f.x = F.(G.x) by FUNCT_1:13
.= F.(((b-x)*0 + (x-a)*1)/(b-a)) by A2,A8,A1,TREAL_1:def 4
.= (1 - X)*c + X * d by A3,A4,A7,TREAL_1:def 3
.= ((d - c)/(b - a)) * (x - a) + c by XCMPLX_1:234;
hence thesis;
end;
theorem Th36:
for f1,f2 being Function of [:I[01],I[01]:],I[01] st f1 is
continuous & f2 is continuous & (for p being Point of [:I[01],I[01]:] holds f1.
p * f2.p is Point of I[01]) holds ex g being Function of [:I[01],I[01]:],I[01]
st (for p being Point of [:I[01],I[01]:],r1,r2 being Real st f1.p=r1 &
f2.p=r2 holds g.p=r1*r2) & g is continuous
proof
reconsider A = [.0,1.] as non empty Subset of R^1 by TOPMETR:17,XXREAL_1:1;
set X = [:I[01],I[01]:];
let f1,f2 be Function of [:I[01],I[01]:],I[01];
assume that
A1: f1 is continuous & f2 is continuous and
A2: for p being Point of [:I[01],I[01]:] holds f1.p * f2.p is Point of I[01];
reconsider f19 = f1, f29 = f2 as Function of X, R^1 by BORSUK_1:40,FUNCT_2:7
,TOPMETR:17;
f19 is continuous & f29 is continuous by A1,PRE_TOPC:26;
then consider g being Function of X,R^1 such that
A3: for p being Point of X,r1,r2 being Real st f19.p=r1 & f29.p=
r2 holds g.p=r1*r2 and
A4: g is continuous by JGRAPH_2:25;
A5: rng g c= [.0,1.]
proof
let x be object;
assume x in rng g;
then consider y being object such that
A6: y in dom g and
A7: x = g.y by FUNCT_1:def 3;
reconsider y as Point of X by A6;
g.y = f1.y * f2.y by A3;
then g.y is Point of I[01] by A2;
hence thesis by A7,BORSUK_1:40;
end;
[.0,1.] = the carrier of R^1|A & dom g = the carrier of X by FUNCT_2:def 1
,PRE_TOPC:8;
then reconsider g as Function of X, R^1|A by A5,FUNCT_2:2;
R^1 | A = I[01] by BORSUK_1:def 13,TOPMETR:def 6;
then reconsider g as continuous Function of X, I[01] by A4,JGRAPH_1:45;
take g;
thus thesis by A3;
end;
theorem Th37:
for f1,f2 being Function of [:I[01],I[01]:],I[01] st f1 is
continuous & f2 is continuous & (for p being Point of [:I[01],I[01]:] holds f1.
p + f2.p is Point of I[01]) holds ex g being Function of [:I[01],I[01]:],I[01]
st (for p being Point of [:I[01],I[01]:],r1,r2 being Real st f1.p=r1 &
f2.p=r2 holds g.p=r1+r2) & g is continuous
proof
reconsider A = [.0,1.] as non empty Subset of R^1 by TOPMETR:17,XXREAL_1:1;
set X = [:I[01],I[01]:];
let f1,f2 be Function of [:I[01],I[01]:],I[01];
assume that
A1: f1 is continuous & f2 is continuous and
A2: for p being Point of [:I[01],I[01]:] holds f1.p + f2.p is Point of I[01];
reconsider f19 = f1, f29 = f2 as Function of X, R^1 by BORSUK_1:40,FUNCT_2:7
,TOPMETR:17;
f19 is continuous & f29 is continuous by A1,PRE_TOPC:26;
then consider g being Function of X,R^1 such that
A3: for p being Point of X,r1,r2 being Real st f19.p=r1 & f29.p=
r2 holds g.p=r1+r2 and
A4: g is continuous by JGRAPH_2:19;
A5: rng g c= [.0,1.]
proof
let x be object;
assume x in rng g;
then consider y being object such that
A6: y in dom g and
A7: x = g.y by FUNCT_1:def 3;
reconsider y as Point of X by A6;
g.y = f1.y + f2.y by A3;
then g.y is Point of I[01] by A2;
hence thesis by A7,BORSUK_1:40;
end;
[.0,1.] = the carrier of R^1|A & dom g = the carrier of X by FUNCT_2:def 1
,PRE_TOPC:8;
then reconsider g as Function of X, R^1|A by A5,FUNCT_2:2;
R^1 | A = I[01] by BORSUK_1:def 13,TOPMETR:def 6;
then reconsider g as continuous Function of X, I[01] by A4,JGRAPH_1:45;
take g;
thus thesis by A3;
end;
theorem
for f1,f2 being Function of [:I[01],I[01]:],I[01] st f1 is continuous
& f2 is continuous & (for p being Point of [:I[01],I[01]:] holds f1.p - f2.p is
Point of I[01]) holds ex g being Function of [:I[01],I[01]:],I[01] st (for p
being Point of [:I[01],I[01]:],r1,r2 being Real st f1.p=r1 & f2.p=r2
holds g.p=r1-r2) & g is continuous
proof
reconsider A = [.0,1.] as non empty Subset of R^1 by TOPMETR:17,XXREAL_1:1;
set X = [:I[01],I[01]:];
let f1,f2 be Function of [:I[01],I[01]:],I[01];
assume that
A1: f1 is continuous & f2 is continuous and
A2: for p being Point of [:I[01],I[01]:] holds f1.p - f2.p is Point of I[01];
reconsider f19 = f1, f29 = f2 as Function of X, R^1 by BORSUK_1:40,FUNCT_2:7
,TOPMETR:17;
f19 is continuous & f29 is continuous by A1,PRE_TOPC:26;
then consider g being Function of X,R^1 such that
A3: for p being Point of X,r1,r2 being Real st f19.p=r1 & f29.p=
r2 holds g.p=r1-r2 and
A4: g is continuous by JGRAPH_2:21;
A5: rng g c= [.0,1.]
proof
let x be object;
assume x in rng g;
then consider y being object such that
A6: y in dom g and
A7: x = g.y by FUNCT_1:def 3;
reconsider y as Point of X by A6;
g.y = f1.y - f2.y by A3;
then g.y is Point of I[01] by A2;
hence thesis by A7,BORSUK_1:40;
end;
[.0,1.] = the carrier of R^1|A & dom g = the carrier of X by FUNCT_2:def 1
,PRE_TOPC:8;
then reconsider g as Function of X, R^1|A by A5,FUNCT_2:2;
R^1 | A = I[01] by BORSUK_1:def 13,TOPMETR:def 6;
then reconsider g as continuous Function of X, I[01] by A4,JGRAPH_1:45;
take g;
thus thesis by A3;
end;
begin :: Paths
reserve T for non empty TopSpace,
a, b, c, d for Point of T;
theorem Th39:
for P being Path of a,b st P is continuous holds P * L[01]((0,1)
(#),(#)(0,1)) is continuous Function of I[01], T
proof
reconsider g = L[01]((0,1)(#),(#)(0,1)) as Function of I[01], I[01] by
TOPMETR:20;
let P be Path of a,b such that
A1: P is continuous;
reconsider f = P * g as Function of I[01], T;
g is continuous by TOPMETR:20,TREAL_1:8;
then f is continuous by A1;
hence thesis;
end;
theorem Th40:
for X being non empty TopStruct, a, b being Point of X, P being
Path of a,b st P.0 = a & P.1 = b holds (P * L[01]((0,1)(#),(#)(0,1))).0 = b & (
P * L[01]((0,1)(#),(#)(0,1))).1 = a
proof
A1: 0 in [. 0,1 .] by XXREAL_1:1;
set e = L[01]((0,1)(#),(#)(0,1));
let X be non empty TopStruct, a, b be Point of X;
let P be Path of a,b such that
A2: P.0 = a and
A3: P.1 = b;
A4: the carrier of Closed-Interval-TSpace(0,1) = [. 0,1 .] by TOPMETR:18;
e.0 = e.(#)(0,1) by TREAL_1:def 1
.= (0,1)(#) by TREAL_1:9
.= 1 by TREAL_1:def 2;
hence (P * e).0 = b by A3,A4,A1,FUNCT_2:15;
A5: 1 in [. 0,1 .] by XXREAL_1:1;
e.1 = e.(0,1)(#) by TREAL_1:def 2
.= (#)(0,1) by TREAL_1:9
.= 0 by TREAL_1:def 1;
hence thesis by A2,A4,A5,FUNCT_2:15;
end;
theorem Th41:
for P being Path of a,b st P is continuous & P.0 = a & P.1 = b
holds -P is continuous & (-P).0 = b & (-P).1 = a
proof
let P be Path of a,b such that
A1: P is continuous and
A2: P.0 = a & P.1 = b;
A3: (P * L[01]((0,1)(#),(#)(0,1))).1 = a by A2,Th40;
P * L[01]((0,1)(#),(#)(0,1)) is continuous Function of I[01], T & (P *
L[01] ((0,1)(#),(#)(0,1))).0 = b by A1,A2,Th39,Th40;
then b,a are_connected by A3;
hence thesis by BORSUK_2:def 2;
end;
definition
let T be non empty TopSpace, a,b be Point of T;
redefine pred a,b are_connected; :: redefines are_connected (BORSUK_2, definition)
reflexivity
proof
let a be Point of T;
thus a,a are_connected;
end;
symmetry
proof
let a,b be Point of T;
set P = the Path of a,b;
assume
A1: a,b are_connected;
then
A2: P.1 = b by BORSUK_2:def 2;
take -P;
P is continuous & P.0 = a by A1,BORSUK_2:def 2;
hence thesis by A2,Th41;
end;
end;
theorem Th42:
a,b are_connected & b,c are_connected implies a,c are_connected
proof
assume that
A1: a,b are_connected and
A2: b,c are_connected;
set P = the Path of a,b,R = the Path of b,c;
A3: P is continuous & P.0 = a by A1,BORSUK_2:def 2;
take P+R;
A4: R.0 = b & R.1 = c by A2,BORSUK_2:def 2;
P.1 = b & R is continuous by A1,A2,BORSUK_2:def 2;
hence thesis by A3,A4,BORSUK_2:14;
end;
theorem Th43:
a,b are_connected implies for A being Path of a,b holds A = --A
proof
set I = the carrier of I[01];
assume
A1: a,b are_connected;
let A be Path of a,b;
for x being Element of I holds A.x = (--A).x
proof
let x be Element of I;
reconsider z = 1-x as Point of I[01] by JORDAN5B:4;
thus (--A).x = (-A).(1-x) by A1,BORSUK_2:def 6
.= A.(1-z) by A1,BORSUK_2:def 6
.= A.x;
end;
hence thesis by FUNCT_2:63;
end;
theorem
for T being non empty pathwise_connected TopSpace, a, b being Point of
T for A being Path of a,b holds A = --A by Th43,BORSUK_2:def 3;
begin :: Reexamination of a Path Concept
definition
let T be non empty pathwise_connected TopSpace;
let a, b, c be Point of T;
let P be Path of a, b, Q be Path of b, c;
redefine func P + Q means :: redefines + (BORSUK_2, definition)
for t being Point of I[01] holds ( t <= 1/2 implies it.t =
P.(2*t) ) & ( 1/2 <= t implies it.t = Q.(2*t-1) );
compatibility
proof
let X be Path of a, c;
a,b are_connected & b,c are_connected by BORSUK_2:def 3;
hence thesis by BORSUK_2:def 5;
end;
end;
definition
let T be non empty pathwise_connected TopSpace;
let a, b be Point of T;
let P be Path of a, b;
redefine func - P means :: redefines - (BORSUK_2, definition)
:Def3:
for t being Point of I[01] holds it.t = P.(1-t);
compatibility
proof
let X be Path of b, a;
b,a are_connected by BORSUK_2:def 3;
hence thesis by BORSUK_2:def 6;
end;
end;
begin :: Reparametrizations
definition
let T be non empty TopSpace, a, b be Point of T;
let P be Path of a, b;
let f be continuous Function of I[01], I[01];
assume that
A1: f.0 = 0 and
A2: f.1 = 1 and
A3: a, b are_connected;
func RePar (P, f) -> Path of a, b equals
:Def4:
P * f;
coherence
proof
set PF = P * f;
0 in the carrier of I[01] by BORSUK_1:43;
then 0 in dom f by FUNCT_2:def 1;
then
A4: PF.0 = P.(f.0) by FUNCT_1:13
.= a by A1,A3,BORSUK_2:def 2;
1 in the carrier of I[01] by BORSUK_1:43;
then 1 in dom f by FUNCT_2:def 1;
then
A5: PF.1 = P.(f.1) by FUNCT_1:13
.= b by A2,A3,BORSUK_2:def 2;
P is continuous by A3,BORSUK_2:def 2;
hence thesis by A3,A4,A5,BORSUK_2:def 2;
end;
end;
theorem Th45:
for P being Path of a, b, f being continuous Function of I[01],
I[01] st f.0 = 0 & f.1 = 1 & a, b are_connected holds RePar (P, f), P
are_homotopic
proof
set X = [:I[01], I[01]:];
reconsider G2 = pr2 (the carrier of I[01], the carrier of I[01]) as
continuous Function of X, I[01] by YELLOW12:40;
reconsider F2 = pr1 (the carrier of I[01], the carrier of I[01]) as
continuous Function of X, I[01] by YELLOW12:39;
reconsider f3 = pr1 (the carrier of I[01], the carrier of I[01]) as
continuous Function of X, I[01] by YELLOW12:39;
reconsider f4 = pr2 (the carrier of I[01], the carrier of I[01]) as
continuous Function of X, I[01] by YELLOW12:40;
reconsider ID = id I[01] as Path of 0[01], 1[01] by Th8;
let P be Path of a, b, f be continuous Function of I[01], I[01];
assume that
A1: f.0 = 0 and
A2: f.1 = 1 and
A3: a,b are_connected;
reconsider f2 = f * F2 as continuous Function of X, I[01];
set G1 = -ID;
reconsider f1 = G1 * G2 as continuous Function of X, I[01];
A4: for s, t being Point of I[01] holds f1. [s,t] = 1 - t
proof
let s, t be Point of I[01];
A5: 1 - t in the carrier of I[01] by JORDAN5B:4;
[s,t] in [:the carrier of I[01],the carrier of I[01]:] by ZFMISC_1:87;
then [s,t] in dom G2 by FUNCT_2:def 1;
then f1. [s,t] = G1. (G2.(s,t)) by FUNCT_1:13
.= G1. t by FUNCT_3:def 5
.= ID.(1 - t) by Def3
.= 1 - t by A5,FUNCT_1:18;
hence thesis;
end;
for p being Point of X holds f3.p * f4.p is Point of I[01] by Th5;
then consider g2 being Function of X,I[01] such that
A6: for p being Point of X,r1,r2 being Real st f3.p=r1 & f4.p=r2
holds g2.p=r1*r2 and
A7: g2 is continuous by Th36;
for p being Point of X holds f1.p * f2.p is Point of I[01] by Th5;
then consider g1 being Function of X,I[01] such that
A8: for p being Point of X,r1,r2 being Real st f1.p=r1 & f2.p=r2
holds g1.p=r1*r2 and
A9: g1 is continuous by Th36;
A10: for s, t being Point of I[01] holds f2.(s,t) = f.s
proof
let s, t be Point of I[01];
[s,t] in [:the carrier of I[01],the carrier of I[01]:] by ZFMISC_1:87;
then [s,t] in dom F2 by FUNCT_2:def 1;
hence f2.(s,t) = f.(F2.(s,t)) by FUNCT_1:13
.= f.s by FUNCT_3:def 4;
end;
A11: for t, s being Point of I[01] holds g1. [s,t] = (1 - t) * f.s
proof
let t,s be Point of I[01];
f1.(s,t) = 1 - t & f2.(s,t) = f.s by A4,A10;
hence thesis by A8;
end;
A12: for t, s being Point of I[01] holds g2. [s,t] = t * s
proof
let t, s being Point of I[01];
f3.(s,t) = s & f4.(s,t) = t by FUNCT_3:def 4,def 5;
hence thesis by A6;
end;
for p being Point of X holds g1.p + g2.p is Point of I[01]
proof
let p be Point of X;
p in the carrier of [:I[01],I[01]:];
then p in [:the carrier of I[01], the carrier of I[01]:] by BORSUK_1:def 2;
then consider s, t being object such that
A13: s in the carrier of I[01] & t in the carrier of I[01] and
A14: p = [s,t] by ZFMISC_1:def 2;
reconsider s, t as Point of I[01] by A13;
set a = f.s;
per cases;
suppose
A15: f.s <= s;
A16: s <= 1 by BORSUK_1:40,XXREAL_1:1;
A17: t <= 1 by BORSUK_1:40,XXREAL_1:1;
then (1-t)*a+t*s<=s by A15,XREAL_1:172;
then
A18: 0 <= a & (1-t)*a+t*s <= 1 by A16,BORSUK_1:40,XXREAL_0:2,XXREAL_1:1;
0 <= t by BORSUK_1:40,XXREAL_1:1;
then
A19: a<=(1-t)*a+t*s by A15,A17,XREAL_1:173;
g1.p + g2.p = (1 - t) * f.s + g2.p by A11,A14
.= (1 - t) * f.s + t * s by A12,A14;
hence thesis by A19,A18,BORSUK_1:40,XXREAL_1:1;
end;
suppose
A20: a > s;
set j = 1 - t;
A21: a <= 1 by BORSUK_1:40,XXREAL_1:1;
A22: j in the carrier of I[01] by JORDAN5B:4;
then
A23: j <= 1 by BORSUK_1:43;
then (1 - j)*s + j * a <= a by A20,XREAL_1:172;
then
A24: 0 <= s & (1-t)*a+t*s <= 1 by A21,BORSUK_1:40,XXREAL_0:2,XXREAL_1:1;
0 <= j by A22,BORSUK_1:43;
then
A25: s <= (1 - j)*s + j * a by A20,A23,XREAL_1:173;
g1.p + g2.p = (1 - t) * f.s + g2.p by A11,A14
.= (1 - t) * f.s + t * s by A12,A14;
hence thesis by A25,A24,BORSUK_1:40,XXREAL_1:1;
end;
end;
then consider h being Function of X,I[01] such that
A26: for p being Point of X,r1,r2 being Real st g1.p=r1 & g2.p=r2
holds h.p=r1+r2 and
A27: h is continuous by A9,A7,Th37;
A28: for t, s being Point of I[01] holds h. [s,t] = (1 - t) * f.s + t * s
proof
let t, s being Point of I[01];
g1. [s,t] = (1 - t) * f.s & g2. [s,t] = t * s by A11,A12;
hence thesis by A26;
end;
A29: for t being Point of I[01] holds h. [1,t] = 1
proof
reconsider oo = 1 as Point of I[01] by BORSUK_1:43;
let t be Point of I[01];
thus h. [1,t] = (1 - t) * f.oo + t * 1 by A28
.= 1 by A2;
end;
set H = P * h;
A30: dom h = the carrier of [:I[01],I[01]:] by FUNCT_2:def 1
.= [:the carrier of I[01],the carrier of I[01]:] by BORSUK_1:def 2;
set Q = RePar (P,f);
A31: 1 is Point of I[01] by BORSUK_1:43;
A32: for s being Point of I[01] holds h. [s,1] = s
proof
let s be Point of I[01];
thus h. [s,1] = (1 - 1) * f.s + 1 * s by A31,A28
.= s;
end;
A33: 0 is Point of I[01] by BORSUK_1:43;
A34: for s being Point of I[01] holds h. [s,0] = f.s
proof
let s be Point of I[01];
thus h. [s,0] = (1 - 0) * f.s + 0 * s by A33,A28
.= f.s;
end;
A35: for s being Point of I[01] holds H.(s,0) = Q.s & H.(s,1) = P.s
proof
let s be Point of I[01];
s in the carrier of I[01];
then
A36: s in dom f by FUNCT_2:def 1;
0 in the carrier of I[01] by BORSUK_1:43;
then [s,0] in dom h by A30,ZFMISC_1:87;
hence H.(s,0) = P.(h. [s,0]) by FUNCT_1:13
.= P.(f.s) by A34
.= (P * f).s by A36,FUNCT_1:13
.= Q.s by A1,A2,A3,Def4;
1 in the carrier of I[01] by BORSUK_1:43;
then [s,1] in dom h by A30,ZFMISC_1:87;
hence H.(s,1) = P. (h. [s,1]) by FUNCT_1:13
.= P.s by A32;
end;
A37: for t being Point of I[01] holds h. [0,t] = 0
proof
reconsider oo = 0 as Point of I[01] by BORSUK_1:43;
let t be Point of I[01];
thus h. [0,t] = (1 - t) * f.oo + t * 0 by A28
.= 0 by A1;
end;
A38: for t being Point of I[01] holds H.(0,t) = a & H.(1,t) = b
proof
let t be Point of I[01];
0 in the carrier of I[01] by BORSUK_1:43;
then [0,t] in dom h by A30,ZFMISC_1:87;
hence H.(0,t) = P. (h. [0,t]) by FUNCT_1:13
.= P. 0 by A37
.= a by A3,BORSUK_2:def 2;
1 in the carrier of I[01] by BORSUK_1:43;
then [1,t] in dom h by A30,ZFMISC_1:87;
hence H.(1,t) = P. (h. [1,t]) by FUNCT_1:13
.= P. 1 by A29
.= b by A3,BORSUK_2:def 2;
end;
P is continuous by A3,BORSUK_2:def 2;
hence thesis by A27,A35,A38;
end;
theorem
for T being non empty pathwise_connected TopSpace, a, b be Point of T,
P being Path of a, b, f being continuous Function of I[01], I[01] st f.0 = 0 &
f.1 = 1 holds RePar (P, f), P are_homotopic by Th45,BORSUK_2:def 3;
definition
func 1RP -> Function of I[01], I[01] means
:Def5:
for t being Point of I[01]
holds (t <= 1/2 implies it.t = 2 * t) & (t > 1/2 implies it.t = 1);
existence
proof
deffunc G(set) = 1;
deffunc F(Real) = 2 * $1;
defpred P[Real] means $1 <= 1/2;
consider f being Function such that
A1: dom f = the carrier of I[01] & for x being Element of I[01] holds
(P[x] implies f.x = F(x)) & (not P[x] implies f.x = G(x)) from PARTFUN1:sch 4;
for x being object st x in the carrier of I[01] holds f.x in the carrier
of I[01]
proof
let x be object;
assume x in the carrier of I[01];
then reconsider x as Point of I[01];
per cases;
suppose
A2: P[x];
then f.x = 2 * x by A1;
then f.x is Point of I[01] by A2,Th3;
hence thesis;
end;
suppose
not P[x];
then f.x = G(x) by A1;
hence thesis by BORSUK_1:43;
end;
end;
then reconsider f as Function of I[01], I[01] by A1,FUNCT_2:3;
for t being Point of I[01] holds (t <= 1/2 implies f.t = 2 * t) & (t >
1/2 implies f.t = 1) by A1;
hence thesis;
end;
uniqueness
proof
let f1, f2 be Function of I[01], I[01];
assume that
A3: for t being Point of I[01] holds (t <= 1/2 implies f1.t = 2 * t)
& (t > 1/2 implies f1.t = 1) and
A4: for t being Point of I[01] holds (t <= 1/2 implies f2.t = 2 * t)
& (t > 1/2 implies f2.t = 1);
for t being Point of I[01] holds f1.t = f2.t
proof
let t be Point of I[01];
per cases;
suppose
A5: t <= 1/2;
then f1.t = 2 * t by A3
.= f2.t by A4,A5;
hence thesis;
end;
suppose
A6: t > 1/2;
then f1.t = 1 by A3
.= f2.t by A4,A6;
hence thesis;
end;
end;
hence thesis by FUNCT_2:63;
end;
end;
registration
cluster 1RP -> continuous;
coherence
proof
A1: 1/2 is Point of I[01] by BORSUK_1:43;
1 is Point of I[01] by BORSUK_1:43;
then reconsider B = [.1/2,1.] as non empty compact Subset of I[01] by A1,
BORSUK_4:24;
0 is Point of I[01] by BORSUK_1:43;
then reconsider A = [.0,1/2.] as non empty compact Subset of I[01] by A1,
BORSUK_4:24;
set T1 = I[01]|A, T2 = I[01]|B, T = I[01];
reconsider g = T2 --> 1[01] as continuous Function of T2, I[01];
T1 = Closed-Interval-TSpace (0,1/2) by TOPMETR:24;
then reconsider
f = L[01](0,1/2,0,1) as continuous Function of T1, I[01] by Th34,TOPMETR:20
;
A2: for p be set st p in ([#] T1) /\ ([#] T2) holds f.p = g.p
proof
let p be set;
assume p in ([#] T1) /\ ([#] T2);
then p in [.0,1/2.] /\ ([#] T2) by PRE_TOPC:def 5;
then p in [.0,1/2.] /\ [.1/2,1.] by PRE_TOPC:def 5;
then p in {1/2} by XXREAL_1:418;
then
A3: p = 1/2 by TARSKI:def 1;
then p in [.1/2,1.] by XXREAL_1:1;
then
A4: p in the carrier of T2 by PRE_TOPC:8;
f.p = ((1 - 0)/(1/2 - 0)) * (1/2 - 0) + 0 by A3,Th35
.= g.p by A4,BORSUK_1:def 15,FUNCOP_1:7;
hence thesis;
end;
A5: for x being Element of I[01] holds 1RP.x = (f +* g).x
proof
let x be Element of I[01];
A6: dom g = the carrier of T2 by FUNCT_2:def 1
.= [.1/2,1.] by PRE_TOPC:8;
per cases by XXREAL_0:1;
suppose
A7: x < 1/2;
0 <= x by BORSUK_1:43;
then
A8: f.x = ((1 - 0)/(1/2 - 0)) * (x - 0) + 0 by A7,Th35
.= (1/(1/2)) * x;
A9: not x in dom g by A6,A7,XXREAL_1:1;
thus 1RP.x = 2 * x by A7,Def5
.= (f +* g).x by A9,A8,FUNCT_4:11;
end;
suppose
A10: x = 1/2;
then
A11: x in dom g by A6,XXREAL_1:1;
thus 1RP.x = 2 * (1/2) by A10,Def5
.= g.x by A11,BORSUK_1:def 15,FUNCOP_1:7
.= (f +* g).x by A11,FUNCT_4:13;
end;
suppose
A12: x > 1/2;
x <= 1 by BORSUK_1:43;
then
A13: x in dom g by A6,A12,XXREAL_1:1;
thus 1RP.x = 1 by A12,Def5
.= g.x by A13,BORSUK_1:def 15,FUNCOP_1:7
.= (f +* g).x by A13,FUNCT_4:13;
end;
end;
([#] T1) \/ ([#] T2) = [.0,1/2.] \/ ([#] T2) by PRE_TOPC:def 5
.= [.0,1/2.] \/ [.1/2,1.] by PRE_TOPC:def 5
.= [#] T by BORSUK_1:40,XXREAL_1:174;
then
ex h being Function of I[01], I[01] st h = f +* g & h is continuous by A2,
BORSUK_2:1;
hence thesis by A5,FUNCT_2:63;
end;
end;
theorem Th47:
1RP.0 = 0 & 1RP.1 = 1
proof
reconsider x = 0, y = 1 as Point of I[01] by BORSUK_1:43;
thus 1RP.0 = 2*x by Def5
.= 0;
thus 1RP.1 = 1RP.y .= 1 by Def5;
end;
definition
func 2RP -> Function of I[01], I[01] means
:Def6:
for t being Point of I[01]
holds (t <= 1/2 implies it.t = 0) & (t > 1/2 implies it.t = 2 * t - 1);
existence
proof
deffunc F(set) = 0;
deffunc G(Real) = 2 * $1 - 1;
defpred P[Real] means $1 <= 1/2;
consider f being Function such that
A1: dom f = the carrier of I[01] & for x being Element of I[01] holds
(P[x] implies f.x = F(x)) & (not P[x] implies f.x = G(x)) from PARTFUN1:sch 4;
for x being object st x in the carrier of I[01] holds f.x in the carrier
of I[01]
proof
let x be object;
assume x in the carrier of I[01];
then reconsider x as Point of I[01];
per cases;
suppose
P[x];
then f.x = 0 by A1;
hence thesis by BORSUK_1:43;
end;
suppose
A2: not P[x];
then f.x = G(x) by A1;
then f.x is Point of I[01] by A2,Th4;
hence thesis;
end;
end;
then reconsider f as Function of I[01], I[01] by A1,FUNCT_2:3;
for t being Point of I[01] holds (t <= 1/2 implies f.t = 0) & (t > 1/2
implies f.t = 2 * t - 1) by A1;
hence thesis;
end;
uniqueness
proof
let f1, f2 be Function of I[01], I[01];
assume that
A3: for t being Point of I[01] holds (t <= 1/2 implies f1.t = 0) & (t
> 1/2 implies f1.t = 2 * t - 1) and
A4: for t being Point of I[01] holds (t <= 1/2 implies f2.t = 0) & (t
> 1/2 implies f2.t = 2 * t - 1);
for t being Point of I[01] holds f1.t = f2.t
proof
let t be Point of I[01];
per cases;
suppose
A5: t <= 1/2;
then f1.t = 0 by A3
.= f2.t by A4,A5;
hence thesis;
end;
suppose
A6: t > 1/2;
then f1.t = 2 * t - 1 by A3
.= f2.t by A4,A6;
hence thesis;
end;
end;
hence thesis by FUNCT_2:63;
end;
end;
registration
cluster 2RP -> continuous;
coherence
proof
A1: 1/2 is Point of I[01] by BORSUK_1:43;
1 is Point of I[01] by BORSUK_1:43;
then reconsider B = [.1/2,1.] as non empty compact Subset of I[01] by A1,
BORSUK_4:24;
0 is Point of I[01] by BORSUK_1:43;
then reconsider A = [.0,1/2.] as non empty compact Subset of I[01] by A1,
BORSUK_4:24;
set T1 = I[01]|A, T2 = I[01]|B, T = I[01];
reconsider g = T1 --> 0[01] as continuous Function of T1, I[01];
T2 = Closed-Interval-TSpace (1/2,1) by TOPMETR:24;
then reconsider
f = L[01](1/2,1,0,1) as continuous Function of T2, I[01] by Th34,TOPMETR:20
;
A2: for p be set st p in ([#] T2) /\ ([#] T1) holds f.p = g.p
proof
let p be set;
assume p in ([#] T2) /\ ([#] T1);
then p in [.0,1/2.] /\ ([#] T2) by PRE_TOPC:def 5;
then p in [.0,1/2.] /\ [.1/2,1.] by PRE_TOPC:def 5;
then p in {1/2} by XXREAL_1:418;
then
A3: p = 1/2 by TARSKI:def 1;
then p in [.0,1/2.] by XXREAL_1:1;
then
A4: p in the carrier of T1 by PRE_TOPC:8;
f.p = ((1 - 0)/(1 - 1/2)) * (1/2 - 1/2) + 0 by A3,Th35
.= g.p by A4,BORSUK_1:def 14,FUNCOP_1:7;
hence thesis;
end;
A5: for x being Element of I[01] holds 2RP.x = (g +* f).x
proof
let x be Element of I[01];
A6: dom f = the carrier of T2 by FUNCT_2:def 1
.= [.1/2,1.] by PRE_TOPC:8;
per cases by XXREAL_0:1;
suppose
A7: x > 1/2;
1 >= x by BORSUK_1:43;
then
A8: f.x = ((1 - 0)/(1 - 1/2)) * (x - 1/2) + 0 by A7,Th35
.= 2 * x - 1;
x <= 1 by BORSUK_1:43;
then
A9: x in dom f by A6,A7,XXREAL_1:1;
thus 2RP.x = 2 * x - 1 by A7,Def6
.= (g +* f).x by A9,A8,FUNCT_4:13;
end;
suppose
A10: x = 1/2;
then
A11: x in dom f by A6,XXREAL_1:1;
thus 2RP.x = ((1 - 0)/(1 - 1/2)) * (1/2 - 1/2) + 0 by A10,Def6
.= f.x by A10,Th35
.= (g +* f).x by A11,FUNCT_4:13;
end;
suppose
A12: x < 1/2;
x >= 0 by BORSUK_1:43;
then x in [.0,1/2.] by A12,XXREAL_1:1;
then
A13: x in the carrier of T1 by PRE_TOPC:8;
A14: not x in dom f by A6,A12,XXREAL_1:1;
thus 2RP.x = 0 by A12,Def6
.= g.x by A13,BORSUK_1:def 14,FUNCOP_1:7
.= (g +* f).x by A14,FUNCT_4:11;
end;
end;
([#] T2) \/ ([#] T1) = [.0,1/2.] \/ ([#] T2) by PRE_TOPC:def 5
.= [.0,1/2.] \/ [.1/2,1.] by PRE_TOPC:def 5
.= [#] T by BORSUK_1:40,XXREAL_1:174;
then
ex h being Function of I[01], I[01] st h = g +* f & h is continuous by A2,
BORSUK_2:1;
hence thesis by A5,FUNCT_2:63;
end;
end;
theorem Th48:
2RP.0 = 0 & 2RP.1 = 1
proof
reconsider x = 0, y = 1 as Point of I[01] by BORSUK_1:43;
thus 2RP.0 = 2RP.x .= 0 by Def6;
thus 2RP.1 = 2 * y - 1 by Def6
.= 1;
end;
definition
func 3RP -> Function of I[01], I[01] means
:Def7:
for x being Point of I[01]
holds (x <= 1/2 implies it.x = 1/2 * x) & (x > 1/2 & x <= 3/4 implies it.x = x
- 1/4) & (x > 3/4 implies it.x = 2 * x - 1);
existence
proof
deffunc H(Real) = 2 * $1 - 1;
deffunc G(Real) = $1 - 1/4;
deffunc F(Real) = 1/2 * $1;
defpred R[Real] means $1 > 3/4;
defpred Q[Real] means $1 > 1/2 & $1 <= 3/4;
defpred P[Real] means $1 <= 1/2;
A1: for c being Element of I[01] holds P[c] or Q[c] or R[c];
A2: for c being Element of I[01] holds (P[c] implies not Q[c]) & (P[c]
implies not R[c]) & (Q[c] implies not R[c]) by XXREAL_0:2;
consider f being Function such that
A3: dom f = the carrier of I[01] & for c being Element of I[01] holds
(P[c] implies f.c = F(c)) & (Q[c] implies f.c = G(c)) & (R[c] implies f.c = H(c
)) from ExFunc3CondD(A2,A1);
for x being object st x in the carrier of I[01] holds f.x in the carrier
of I[01]
proof
let x be object;
assume x in the carrier of I[01];
then reconsider x as Point of I[01];
per cases;
suppose
P[x];
then f.x = 1/2 * x by A3;
then f.x is Point of I[01] by Th6;
hence thesis;
end;
suppose
A4: Q[x];
then f.x = G(x) by A3;
then f.x is Point of I[01] by A4,Th7;
hence thesis;
end;
suppose
A5: R[x];
then f.x = 2 * x - 1 by A3;
then f.x is Point of I[01] by A5,Th4,XXREAL_0:2;
hence thesis;
end;
end;
then reconsider f as Function of I[01], I[01] by A3,FUNCT_2:3;
for x being Point of I[01] holds (x <= 1/2 implies f.x = 1/2 * x) & (
x > 1/2 & x <= 3/4 implies f.x = x - 1/4) & (x > 3/4 implies f.x = 2 * x - 1)
by A3;
hence thesis;
end;
uniqueness
proof
let f1, f2 be Function of I[01], I[01];
assume that
A6: for x being Point of I[01] holds (x <= 1/2 implies f1.x = 1/2 * x
) & (x > 1/2 & x <= 3/4 implies f1.x = x - 1/4) & (x > 3/4 implies f1.x = 2 * x
- 1) and
A7: for x being Point of I[01] holds (x <= 1/2 implies f2.x = 1/2 * x
) & (x > 1/2 & x <= 3/4 implies f2.x = x - 1/4) & (x > 3/4 implies f2.x = 2 * x
- 1);
for x being Point of I[01] holds f1.x = f2.x
proof
let x be Point of I[01];
per cases;
suppose
A8: x <= 1/2;
then f1.x = 1/2 * x by A6
.= f2.x by A7,A8;
hence thesis;
end;
suppose
A9: x > 1/2 & x <= 3/4;
then f1.x = x - 1/4 by A6
.= f2.x by A7,A9;
hence thesis;
end;
suppose
A10: x > 3/4;
then f1.x = 2 * x - 1 by A6
.= f2.x by A7,A10;
hence thesis;
end;
end;
hence thesis by FUNCT_2:63;
end;
end;
registration
cluster 3RP -> continuous;
coherence
proof
A1: 1/2 is Point of I[01] by BORSUK_1:43;
A2: 3/4 is Point of I[01] by BORSUK_1:43;
then reconsider
B = [.1/2,3/4.] as non empty compact Subset of I[01] by A1,BORSUK_4:24;
A3: 0 is Point of I[01] by BORSUK_1:43;
then reconsider A = [.0,1/2.] as non empty compact Subset of I[01] by A1,
BORSUK_4:24;
reconsider G = [.0,3/4.] as non empty compact Subset of I[01] by A3,A2,
BORSUK_4:24;
A4: 1/4 is Point of I[01] by BORSUK_1:43;
then reconsider
E = [.1/4,1/2.] as non empty compact Subset of I[01] by A1,BORSUK_4:24;
reconsider F = [.0,1/4.] as non empty compact Subset of I[01] by A3,A4,
BORSUK_4:24;
A5: 1 is Point of I[01] by BORSUK_1:43;
then reconsider C = [.3/4,1.] as non empty compact Subset of I[01] by A2,
BORSUK_4:24;
reconsider D = [.1/2,1.] as non empty compact Subset of I[01] by A1,A5,
BORSUK_4:24;
set T = I[01];
set T1 = T|A, T2 = T|B, T3 = T|C, T4 = T|D, T5 = T|E, T6 = T|F;
set f = L[01](0,1/2,0,1/4);
set g = L[01](1/2,3/4,1/4,1/2);
set h = L[01](3/4,1,1/2,1);
reconsider TT1 = T1, TT2 = T2 as SubSpace of T|G by TOPMETR:22,XXREAL_1:34;
Closed-Interval-TSpace (3/4,1) = T3 & Closed-Interval-TSpace (1/2,1) =
T4 by TOPMETR:24;
then reconsider h as continuous Function of T3, T4 by Th34;
reconsider h as continuous Function of T3, T by JORDAN6:3;
A6: for x being Point of T3 holds h.x = 2 * x - 1
proof
let x be Point of T3;
x in the carrier of T3;
then x in C by PRE_TOPC:8;
then 3/4 <= x & x <= 1 by XXREAL_1:1;
then h.x = ((1 - 1/2)/(1 - 3/4)) * (x - 3/4) + 1/2 by Th35
.= 2 * x - 1;
hence thesis;
end;
Closed-Interval-TSpace (0,1/4) = T6 & Closed-Interval-TSpace (0,1/2) =
T1 by TOPMETR:24;
then reconsider f as continuous Function of T1, T6 by Th34;
Closed-Interval-TSpace (1/4,1/2) = T5 & Closed-Interval-TSpace (1/2,3/
4) = T2 by TOPMETR:24;
then reconsider g as continuous Function of T2, T5 by Th34;
reconsider g as continuous Function of T2, T by JORDAN6:3;
reconsider f as continuous Function of T1, T by JORDAN6:3;
set f1 = f, g1 = g;
A7: for x being Point of T2 holds g.x = x - 1/4
proof
let x be Point of T2;
x in the carrier of T2;
then x in B by PRE_TOPC:8;
then 1/2 <= x & x <= 3/4 by XXREAL_1:1;
then g.x = ((1/2 - 1/4)/(3/4 - 1/2)) * (x - 1/2) + 1/4 by Th35
.= x - 1/4;
hence thesis;
end;
A8: ([#] TT1) /\ ([#] TT2) = A /\ ([#] TT2) by PRE_TOPC:def 5
.= A /\ B by PRE_TOPC:def 5
.= {1/2} by XXREAL_1:418;
A9: for p be set st p in ([#] TT1) /\ ([#] TT2) holds f1.p = g1.p
proof
let p be set;
assume p in ([#] TT1) /\ ([#] TT2);
then
A10: p = 1/2 by A8,TARSKI:def 1;
then reconsider p as Point of I[01] by BORSUK_1:40,XXREAL_1:1;
f1.p = ((1/4 - 0)/(1/2 - 0)) * (p - 0) + 0 by A10,Th35
.= ((1/2 - 1/4)/(3/4 - 1/2)) * (p - 1/2) + 1/4 by A10
.= g1.p by A10,Th35;
hence thesis;
end;
([#] TT1) \/ ([#] TT2) = A \/ ([#] TT2) by PRE_TOPC:def 5
.= A \/ B by PRE_TOPC:def 5
.= [.0,3/4.] by XXREAL_1:174
.= [#] (T|G) by PRE_TOPC:def 5;
then consider FF being Function of T|G, T such that
A11: FF = f1 +* g1 and
A12: FF is continuous by A9,BORSUK_2:1;
A13: ([#] (T|G)) /\ ([#] T3) = G /\ ([#] T3) by PRE_TOPC:def 5
.= G /\ C by PRE_TOPC:def 5
.= {3/4} by XXREAL_1:418;
A14: for p be set st p in ([#] (T|G)) /\ ([#] T3) holds FF.p = h.p
proof
let p be set;
assume p in ([#] (T|G)) /\ ([#] T3);
then
A15: p = 3/4 by A13,TARSKI:def 1;
then reconsider p as Point of T by BORSUK_1:43;
p in [.1/2,3/4.] by A15,XXREAL_1:1;
then p in the carrier of T2 by PRE_TOPC:8;
then p in dom g by FUNCT_2:def 1;
then FF.p = g.p by A11,FUNCT_4:13
.= 1/2 by A15,Th33
.= h.p by A15,Th33;
hence thesis;
end;
([#] (T|G)) \/ ([#] T3) = G \/ ([#] T3) by PRE_TOPC:def 5
.= G \/ C by PRE_TOPC:def 5
.= [#] T by BORSUK_1:40,XXREAL_1:174;
then consider HH being Function of T, T such that
A16: HH = FF +* h and
A17: HH is continuous by A12,A14,BORSUK_2:1;
A18: for x being Point of T1 holds f.x = 1/2 * x
proof
let x be Point of T1;
x in the carrier of T1;
then x in A by PRE_TOPC:8;
then 0 <= x & x <= 1/2 by XXREAL_1:1;
then f.x = ((1/4 - 0)/(1/2 - 0)) * (x - 0) + 0 by Th35
.= 1/2 * x;
hence thesis;
end;
for x being Element of T holds HH.x = 3RP.x
proof
let x be Element of T;
A19: 0 <= x by BORSUK_1:43;
A20: x <= 1 by BORSUK_1:43;
per cases by XXREAL_0:1;
suppose
A21: x < 1/2;
then not x in [.1/2,3/4.] by XXREAL_1:1;
then not x in the carrier of T2 by PRE_TOPC:8;
then
A22: not x in dom g;
x in [.0,1/2.] by A19,A21,XXREAL_1:1;
then
A23: x is Point of T1 by PRE_TOPC:8;
x < 3/4 by A21,XXREAL_0:2;
then not x in [.3/4,1.] by XXREAL_1:1;
then not x in the carrier of T3 by PRE_TOPC:8;
then not x in dom h;
then HH.x = FF.x by A16,FUNCT_4:11
.= f.x by A11,A22,FUNCT_4:11
.= 1/2 * x by A18,A23
.= 3RP.x by A21,Def7;
hence thesis;
end;
suppose
A24: x = 1/2;
then x in [.1/2,3/4.] by XXREAL_1:1;
then x in the carrier of T2 by PRE_TOPC:8;
then
A25: x in dom g by FUNCT_2:def 1;
not x in [.3/4,1.] by A24,XXREAL_1:1;
then not x in the carrier of T3 by PRE_TOPC:8;
then not x in dom h;
then HH.x = FF.x by A16,FUNCT_4:11
.= g.x by A11,A25,FUNCT_4:13
.= 1/2 * x by A24,Th33
.= 3RP.x by A24,Def7;
hence thesis;
end;
suppose
A26: x > 1/2 & x < 3/4;
then x in [.1/2,3/4.] by XXREAL_1:1;
then
A27: x in the carrier of T2 by PRE_TOPC:8;
then
A28: x in dom g by FUNCT_2:def 1;
not x in [.3/4,1.] by A26,XXREAL_1:1;
then not x in the carrier of T3 by PRE_TOPC:8;
then not x in dom h;
then HH.x = FF.x by A16,FUNCT_4:11
.= g.x by A11,A28,FUNCT_4:13
.= x - 1/4 by A7,A27
.= 3RP.x by A26,Def7;
hence thesis;
end;
suppose
A29: x = 3/4;
then x in [.3/4,1.] by XXREAL_1:1;
then x in the carrier of T3 by PRE_TOPC:8;
then x in dom h by FUNCT_2:def 1;
then HH.x = h.x by A16,FUNCT_4:13
.= x - 1/4 by A29,Th33
.= 3RP.x by A29,Def7;
hence thesis;
end;
suppose
A30: x > 3/4;
then x in [.3/4,1.] by A20,XXREAL_1:1;
then
A31: x in the carrier of T3 by PRE_TOPC:8;
then x in dom h by FUNCT_2:def 1;
then HH.x = h.x by A16,FUNCT_4:13
.= 2 * x - 1 by A6,A31
.= 3RP.x by A30,Def7;
hence thesis;
end;
end;
hence thesis by A17,FUNCT_2:63;
end;
end;
theorem Th49:
3RP.0 = 0 & 3RP.1 = 1
proof
0 is Point of I[01] by BORSUK_1:43;
hence 3RP.0 = 1/2 * 0 by Def7
.= 0;
1 is Point of I[01] by BORSUK_1:43;
hence 3RP.1 = 2 * 1 - 1 by Def7
.= 1;
end;
theorem Th50:
for P being Path of a, b, Q being constant Path of b, b st a,b
are_connected holds RePar (P, 1RP) = P + Q
proof
let P be Path of a, b, Q be constant Path of b, b;
set f = RePar (P, 1RP), g = P + Q;
assume
A1: a, b are_connected;
A2: b, b are_connected;
for p being Element of I[01] holds f.p = g.p
proof
0 in the carrier of I[01] by BORSUK_1:43;
then
A3: 0 in dom Q by FUNCT_2:def 1;
let p be Element of I[01];
p in the carrier of I[01];
then
A4: p in dom 1RP by FUNCT_2:def 1;
A5: f.p = (P * 1RP).p by A1,Def4,Th47
.= P. (1RP.p) by A4,FUNCT_1:13;
per cases;
suppose
A6: p <= 1/2;
then f.p = P.(2*p) by A5,Def5
.= g.p by A1,A6,BORSUK_2:def 5;
hence thesis;
end;
suppose
A7: p > 1/2;
then 2*p - 1 is Point of I[01] by Th4;
then 2*p - 1 in the carrier of I[01];
then
A8: 2*p - 1 in dom Q by FUNCT_2:def 1;
f.p = P.1 by A5,A7,Def5
.= b by A1,BORSUK_2:def 2
.= Q.0 by A2,BORSUK_2:def 2
.= Q.(2*p - 1) by A3,A8,FUNCT_1:def 10
.= g.p by A1,A7,BORSUK_2:def 5;
hence thesis;
end;
end;
hence thesis by FUNCT_2:63;
end;
theorem Th51:
for P being Path of a, b, Q being constant Path of a, a st a,b
are_connected holds RePar (P, 2RP) = Q + P
proof
let P be Path of a, b, Q be constant Path of a, a;
assume
A1: a,b are_connected;
set f = RePar (P, 2RP), g = Q + P;
A2: a,a are_connected;
for p being Element of I[01] holds f.p = g.p
proof
0 in the carrier of I[01] by BORSUK_1:43;
then
A3: 0 in dom Q by FUNCT_2:def 1;
let p be Element of I[01];
p in the carrier of I[01];
then
A4: p in dom 2RP by FUNCT_2:def 1;
A5: f.p = (P * 2RP).p by A1,Def4,Th48
.= P. (2RP.p) by A4,FUNCT_1:13;
per cases;
suppose
A6: p <= 1/2;
then 2*p is Point of I[01] by Th3;
then 2*p in the carrier of I[01];
then
A7: 2*p in dom Q by FUNCT_2:def 1;
f.p = P.0 by A5,A6,Def6
.= a by A1,BORSUK_2:def 2
.= Q.0 by A2,BORSUK_2:def 2
.= Q.(2*p) by A3,A7,FUNCT_1:def 10
.= g.p by A1,A6,BORSUK_2:def 5;
hence thesis;
end;
suppose
A8: p > 1/2;
then f.p = P.(2*p - 1) by A5,Def6
.= g.p by A1,A8,BORSUK_2:def 5;
hence thesis;
end;
end;
hence thesis by FUNCT_2:63;
end;
theorem Th52:
for P being Path of a, b, Q being Path of b, c, R being Path of
c, d st a,b are_connected & b,c are_connected & c,d are_connected holds RePar (
P + Q + R, 3RP) = P + (Q + R)
proof
let P be Path of a, b, Q be Path of b, c, R be Path of c, d;
assume that
A1: a,b are_connected and
A2: b,c are_connected and
A3: c,d are_connected;
set F = P + Q + R;
set f = RePar (F, 3RP), g = P + (Q + R);
A4: a,c are_connected by A1,A2,Th42;
A5: b,d are_connected by A2,A3,Th42;
for x being Point of I[01] holds f.x = g.x
proof
let x be Point of I[01];
x in the carrier of I[01];
then
A6: x in dom 3RP by FUNCT_2:def 1;
A7: f.x = (F*3RP).x by A3,A4,Def4,Th42,Th49
.= F.(3RP.x) by A6,FUNCT_1:13;
per cases;
suppose
A8: x <= 1/2;
reconsider y = 1/2 * x as Point of I[01] by Th6;
1/2 * x <= (1/2) * (1/2) by A8,XREAL_1:64;
then
A9: y <= 1/2 by XXREAL_0:2;
reconsider z = 2 * y as Point of I[01];
f.x = F.y by A7,A8,Def7
.= (P + Q).z by A3,A4,A9,BORSUK_2:def 5
.= P.(2 * x) by A1,A2,A8,BORSUK_2:def 5
.= g.x by A1,A5,A8,BORSUK_2:def 5;
hence thesis;
end;
suppose
A10: x > 1/2 & x <= 3/4;
then
A11: 1/2 - 1/4 <= x - 1/4 by XREAL_1:9;
A12: x - 1/4 <= 3/4 - 1/4 by A10,XREAL_1:9;
then x - 1/4 <= 1 by XXREAL_0:2;
then reconsider y = x - 1/4 as Point of I[01] by A11,BORSUK_1:43;
reconsider z = 2 * y as Point of I[01] by A12,Th3;
A13: 2 * y >= 2 * (1/4) by A11,XREAL_1:64;
reconsider w = 2 * x - 1 as Point of I[01] by A10,Th4;
2 * x <= 2 * (3/4) by A10,XREAL_1:64;
then
A14: 2 * x - 1 <= 3/2 - 1 by XREAL_1:9;
f.x = F.y by A7,A10,Def7
.= (P + Q).z by A3,A4,A12,BORSUK_2:def 5
.= Q.(2 * z - 1) by A1,A2,A13,BORSUK_2:def 5
.= Q.(2 * w)
.= (Q + R).w by A2,A3,A14,BORSUK_2:def 5
.= g.x by A1,A5,A10,BORSUK_2:def 5;
hence thesis;
end;
suppose
A15: x > 3/4;
then reconsider w = 2 * x - 1 as Point of I[01] by Th4,XXREAL_0:2;
2 * x > 2 * (3/4) by A15,XREAL_1:68;
then
A16: 2 * x - 1 > 2 * (3/4) - 1 by XREAL_1:14;
reconsider y = 2 * x - 1 as Point of I[01] by A15,Th4,XXREAL_0:2;
A17: x > 1/2 by A15,XXREAL_0:2;
f.x = F.y by A7,A15,Def7
.= R.(2 * y - 1) by A3,A4,A16,BORSUK_2:def 5
.= (Q + R).w by A2,A3,A16,BORSUK_2:def 5
.= g.x by A1,A5,A17,BORSUK_2:def 5;
hence thesis;
end;
end;
hence thesis by FUNCT_2:63;
end;
begin :: Decomposition of the Unit Square
definition
func LowerLeftUnitTriangle -> Subset of [:I[01], I[01]:] means
:Def8:
for x
being set holds x in it iff ex a, b being Point of I[01] st x = [a,b] & b <= 1
- 2 * a;
existence
proof
defpred P[object] means
ex a, b being Point of I[01] st $1 = [a,b] & b <= 1 -
2 * a;
consider X being set such that
A1: for x being object holds x in X iff x in the carrier of [:I[01],
I[01]:] & P[x] from XBOOLE_0:sch 1;
X c= the carrier of [:I[01], I[01]:]
by A1;
then reconsider X as Subset of [:I[01], I[01]:];
take X;
thus thesis by A1;
end;
uniqueness
proof
let X1, X2 be Subset of [:I[01], I[01]:] such that
A2: for x being set holds x in X1 iff ex a, b being Point of I[01] st
x = [a,b] & b <= 1 - 2 * a and
A3: for x being set holds x in X2 iff ex a, b being Point of I[01] st
x = [a,b] & b <= 1 - 2 * a;
X1 = X2
proof
thus X1 c= X2
proof
let x be object;
assume x in X1;
then
ex a, b being Point of I[01] st x = [a,b] & b <= 1 - 2 * a by A2;
hence thesis by A3;
end;
let x be object;
assume x in X2;
then ex a, b being Point of I[01] st x = [a,b] & b <= 1 - 2 * a by A3;
hence thesis by A2;
end;
hence thesis;
end;
end;
notation
synonym IAA for LowerLeftUnitTriangle;
end;
definition
func UpperUnitTriangle -> Subset of [:I[01], I[01]:] means
:Def9:
for x
being set holds x in it iff ex a, b being Point of I[01] st x = [a,b] & b >= 1
- 2 * a & b >= 2 * a - 1;
existence
proof
defpred P[object] means
ex a, b being Point of I[01] st $1 = [a,b] & b >= 1 -
2 * a & b >= 2 * a - 1;
consider X being set such that
A1: for x being object holds x in X iff x in the carrier of [:I[01],
I[01]:] & P[x] from XBOOLE_0:sch 1;
X c= the carrier of [:I[01], I[01]:]
by A1;
then reconsider X as Subset of [:I[01], I[01]:];
take X;
thus thesis by A1;
end;
uniqueness
proof
let X1, X2 be Subset of [:I[01], I[01]:] such that
A2: for x being set holds x in X1 iff ex a, b being Point of I[01] st
x = [a,b] & b >= 1 - 2 * a & b >= 2 * a - 1 and
A3: for x being set holds x in X2 iff ex a, b being Point of I[01] st
x = [a,b] & b >= 1 - 2 * a & b >= 2 * a - 1;
X1 = X2
proof
thus X1 c= X2
proof
let x be object;
assume x in X1;
then
ex a, b being Point of I[01] st x = [a,b] & b >= 1 - 2 * a & b >=
2 * a - 1 by A2;
hence thesis by A3;
end;
let x be object;
assume x in X2;
then
ex a, b being Point of I[01] st x = [a,b] & b >= 1 - 2 * a & b >= 2
* a - 1 by A3;
hence thesis by A2;
end;
hence thesis;
end;
end;
notation
synonym IBB for UpperUnitTriangle;
end;
definition
func LowerRightUnitTriangle -> Subset of [:I[01], I[01]:] means
:Def10:
for
x being set holds x in it iff ex a, b being Point of I[01] st x = [a,b] & b <=
2 * a - 1;
existence
proof
defpred P[object] means
ex a, b being Point of I[01] st $1 = [a,b] & b <= 2 *
a - 1;
consider X being set such that
A1: for x being object holds x in X iff x in the carrier of [:I[01],
I[01]:] & P[x] from XBOOLE_0:sch 1;
X c= the carrier of [:I[01], I[01]:]
by A1;
then reconsider X as Subset of [:I[01], I[01]:];
take X;
thus thesis by A1;
end;
uniqueness
proof
let X1, X2 be Subset of [:I[01], I[01]:] such that
A2: for x being set holds x in X1 iff ex a, b being Point of I[01] st
x = [a,b] & b <= 2 * a - 1 and
A3: for x being set holds x in X2 iff ex a, b being Point of I[01] st
x = [a,b] & b <= 2 * a - 1;
X1 = X2
proof
thus X1 c= X2
proof
let x be object;
assume x in X1;
then
ex a, b being Point of I[01] st x = [a,b] & b <= 2 * a - 1 by A2;
hence thesis by A3;
end;
let x be object;
assume x in X2;
then ex a, b being Point of I[01] st x = [a,b] & b <= 2 * a - 1 by A3;
hence thesis by A2;
end;
hence thesis;
end;
end;
notation
synonym ICC for LowerRightUnitTriangle;
end;
theorem Th53:
IAA = { p where p is Point of [:I[01], I[01]:] : p`2 <= 1 - 2 * (p`1) }
proof
set P = { p where p is Point of [:I[01], I[01]:] : p`2 <= 1 - 2 * (p`1) };
thus IAA c= P
proof
let x be object;
assume
A1: x in IAA;
then reconsider x9 = x as Point of [:I[01], I[01]:];
consider a, b being Point of I[01] such that
A2: x = [a,b] and
A3: b <= 1 - 2 * a by A1,Def8;
x9`1 = a & x9`2 = b by A2;
hence thesis by A3;
end;
let x be object;
assume x in P;
then consider p being Point of [:I[01], I[01]:] such that
A4: p = x and
A5: p`2 <= 1 - 2 * (p`1);
x in the carrier of [:I[01], I[01]:] by A4;
then x in [:the carrier of I[01], the carrier of I[01]:] by BORSUK_1:def 2;
then
A6: x = [x`1, x`2] by MCART_1:21;
p`1 is Point of I[01] & p`2 is Point of I[01] by Th27;
hence thesis by A4,A5,A6,Def8;
end;
theorem Th54:
IBB = { p where p is Point of [:I[01], I[01]:] : p`2 >= 1 - 2 *
(p`1) & p`2 >= 2 * (p`1) - 1 }
proof
set P = { p where p is Point of [:I[01], I[01]:] : p`2 >= 1 - 2 * (p`1) & p
`2 >= 2 * (p`1) - 1 };
thus IBB c= P
proof
let x be object;
assume
A1: x in IBB;
then reconsider x9 = x as Point of [:I[01], I[01]:];
consider a, b being Point of I[01] such that
A2: x = [a,b] and
A3: b >= 1 - 2 * a & b >= 2 * a - 1 by A1,Def9;
x9`1 = a & x9`2 = b by A2;
hence thesis by A3;
end;
let x be object;
assume x in P;
then consider p being Point of [:I[01], I[01]:] such that
A4: p = x and
A5: p`2 >= 1 - 2 * (p`1) & p`2 >= 2 * (p`1) - 1;
x in the carrier of [:I[01], I[01]:] by A4;
then x in [:the carrier of I[01], the carrier of I[01]:] by BORSUK_1:def 2;
then
A6: x = [x`1, x`2] by MCART_1:21;
p`1 is Point of I[01] & p`2 is Point of I[01] by Th27;
hence thesis by A4,A5,A6,Def9;
end;
theorem Th55:
ICC = { p where p is Point of [:I[01], I[01]:] : p`2 <= 2 * (p`1 ) - 1 }
proof
set P = { p where p is Point of [:I[01], I[01]:] : p`2 <= 2 * (p`1) - 1 };
thus ICC c= P
proof
let x be object;
assume
A1: x in ICC;
then reconsider x9 = x as Point of [:I[01], I[01]:];
consider a, b being Point of I[01] such that
A2: x = [a,b] and
A3: b <= 2 * a - 1 by A1,Def10;
x9`1 = a & x9`2 = b by A2;
hence thesis by A3;
end;
let x be object;
assume x in P;
then consider p being Point of [:I[01], I[01]:] such that
A4: p = x and
A5: p`2 <= 2 * (p`1) - 1;
x in the carrier of [:I[01], I[01]:] by A4;
then x in [:the carrier of I[01], the carrier of I[01]:] by BORSUK_1:def 2;
then
A6: x = [x`1, x`2] by MCART_1:21;
p`1 is Point of I[01] & p`2 is Point of I[01] by Th27;
hence thesis by A4,A5,A6,Def10;
end;
registration
cluster IAA -> closed non empty;
coherence by Th24,Th53;
cluster IBB -> closed non empty;
coherence by Th25,Th54;
cluster ICC -> closed non empty;
coherence by Th26,Th55;
end;
theorem Th56:
IAA \/ IBB \/ ICC = [:[.0,1.], [.0,1.]:]
proof
thus IAA \/ IBB \/ ICC c= [:[.0,1.], [.0,1.]:] by Th1;
let x be object;
assume
A1: x in [:[.0,1.], [.0,1.]:];
then reconsider q = x`1, p = x`2 as Point of I[01] by BORSUK_1:40,MCART_1:10;
A2: x = [q,p] by A1,MCART_1:21;
x in IAA or x in IBB or x in ICC
proof
per cases;
suppose
A3: p >= 1 - 2 * q;
now
per cases;
suppose
p >= 2 * q - 1;
hence thesis by A2,A3,Def9;
end;
suppose
p < 2 * q - 1;
hence thesis by A2,Def10;
end;
end;
hence thesis;
end;
suppose
p < 1 - 2 * q;
hence thesis by A2,Def8;
end;
end;
then x in IAA \/ IBB or x in ICC by XBOOLE_0:def 3;
hence thesis by XBOOLE_0:def 3;
end;
theorem Th57:
IAA /\ IBB = { p where p is Point of [:I[01], I[01]:] : p`2 = 1 - 2 * (p`1) }
proof
set KK = { p where p is Point of [:I[01], I[01]:] : p`2 = 1 - 2 * (p`1) };
thus IAA /\ IBB c= KK
proof
let x be object;
assume
A1: x in IAA /\ IBB;
then x in IAA by XBOOLE_0:def 4;
then consider p being Point of [:I[01], I[01]:] such that
A2: x = p and
A3: p`2 <= 1 - 2 * (p`1) by Th53;
x in IBB by A1,XBOOLE_0:def 4;
then
ex q being Point of [:I[01], I[01]:] st x = q & q`2 >= 1 - 2 * (q`1) &
q`2 >= 2 * (q`1) - 1 by Th54;
then p`2 = 1 - 2 * (p`1) by A2,A3,XXREAL_0:1;
hence thesis by A2;
end;
let x be object;
assume x in KK;
then consider p being Point of [:I[01], I[01]:] such that
A4: p = x and
A5: p`2 = 1 - 2 * (p`1);
x in the carrier of [:I[01], I[01]:] by A4;
then
A6: x in [:the carrier of I[01], the carrier of I[01]:] by BORSUK_1:def 2;
then
A7: x = [p`1,p`2] & p`1 in the carrier of I[01] by A4,MCART_1:10,21;
A8: p`2 in the carrier of I[01] by A4,A6,MCART_1:10;
then
A9: x in IAA by A5,A7,Def8;
1 - 2 * p`1 >= 0 by A5,A8,BORSUK_1:43;
then 0 + 2 * p`1 <= 1 by XREAL_1:19;
then (2 * p`1)/2 <= 1/2 by XREAL_1:72;
then 2 * p`1 - 1 <= 0 & 0 <= 1 - 2 * (p`1) by XREAL_1:217,218;
then x in IBB by A5,A7,A8,Def9;
hence thesis by A9,XBOOLE_0:def 4;
end;
theorem Th58:
ICC /\ IBB = { p where p is Point of [:I[01], I[01]:] : p`2 = 2 * (p`1) - 1 }
proof
set KK = { p where p is Point of [:I[01], I[01]:] : p`2 = 2 * (p`1) - 1 };
thus ICC /\ IBB c= KK
proof
let x be object;
assume
A1: x in ICC /\ IBB;
then x in ICC by XBOOLE_0:def 4;
then consider p being Point of [:I[01], I[01]:] such that
A2: x = p and
A3: p`2 <= 2 * (p`1) - 1 by Th55;
x in IBB by A1,XBOOLE_0:def 4;
then
ex q being Point of [:I[01], I[01]:] st x = q & q`2 >= 1 - 2 * (q`1) &
q`2 >= 2 * (q`1) - 1 by Th54;
then p`2 = 2 * (p`1) - 1 by A2,A3,XXREAL_0:1;
hence thesis by A2;
end;
let x be object;
assume x in KK;
then consider p being Point of [:I[01], I[01]:] such that
A4: p = x and
A5: p`2 = 2 * (p`1) - 1;
x in the carrier of [:I[01], I[01]:] by A4;
then
A6: x in [:the carrier of I[01], the carrier of I[01]:] by BORSUK_1:def 2;
then
A7: x = [p`1,p`2] & p`1 in the carrier of I[01] by A4,MCART_1:10,21;
A8: p`2 in the carrier of I[01] by A4,A6,MCART_1:10;
then
A9: x in ICC by A5,A7,Def10;
2 * p`1 - 1 >= 0 by A5,A8,BORSUK_1:43;
then 2 * p`1 >= 0 + 1 by XREAL_1:19;
then (2 * p`1)/2 >= 1/2 by XREAL_1:72;
then 2 * p`1 - 1 >= 0 & 0 >= 1 - 2 * (p`1) by XREAL_1:219,220;
then x in IBB by A5,A7,A8,Def9;
hence thesis by A9,XBOOLE_0:def 4;
end;
theorem Th59:
for x being Point of [:I[01], I[01]:] st x in IAA holds x`1 <= 1 /2
proof
set GG = [:I[01], I[01]:];
let x be Point of GG;
assume x in IAA;
then consider a, b being Point of I[01] such that
A1: x = [a,b] and
A2: b <= 1 - 2 * a by Def8;
b >= 0 by BORSUK_1:43;
then 1 >= 0 + 2 * a by A2,XREAL_1:19;
then
A3: 1/2 >= (2 * a)/2 by XREAL_1:72;
thus thesis by A1,A3;
end;
theorem Th60:
for x being Point of [:I[01], I[01]:] st x in ICC holds x`1 >= 1 /2
proof
set GG = [:I[01], I[01]:];
let x be Point of GG;
assume x in ICC;
then consider a, b being Point of I[01] such that
A1: x = [a,b] and
A2: b <= 2 * a - 1 by Def10;
b >= 0 by BORSUK_1:43;
then 0 + 1 <= 2 * a by A2,XREAL_1:19;
then
A3: 1/2 <= (2 * a)/2 by XREAL_1:72;
thus thesis by A1,A3;
end;
theorem Th61:
for x being Point of I[01] holds [0,x] in IAA
proof
let x be Point of I[01];
0 is Point of I[01] & x <= 1 - 2 * 0 by BORSUK_1:43;
hence thesis by Def8;
end;
theorem Th62:
for s being set holds [0,s] in IBB implies s = 1
proof
let s be set;
assume [0,s] in IBB;
then consider a, b being Point of I[01] such that
A1: [0,s] = [a,b] and
A2: b >= 1 - 2 * a and
b >= 2 * a - 1 by Def9;
A3: b <= 1 by BORSUK_1:43;
a = 0 & b = s by A1,XTUPLE_0:1;
hence thesis by A2,A3,XXREAL_0:1;
end;
theorem Th63:
for s being set holds [s,1] in ICC implies s = 1
proof
let s be set;
assume [s,1] in ICC;
then consider a, b being Point of I[01] such that
A1: [s,1] = [a,b] and
A2: b <= 2 * a - 1 by Def10;
b = 1 by A1,XTUPLE_0:1;
then 1 + 1 <= 2 * a by A2,XREAL_1:19;
then
A3: 2/2 <= (2 * a)/2 by XREAL_1:72;
a <= 1 & a = s by A1,BORSUK_1:43,XTUPLE_0:1;
hence thesis by A3,XXREAL_0:1;
end;
theorem Th64:
[0,1] in IBB
proof
A1: 1 >= 1 - 2 * 0 & 1 >= 2 * 0 - 1;
0 is Point of I[01] & 1 is Point of I[01] by BORSUK_1:43;
hence thesis by A1,Def9;
end;
theorem Th65:
for x being Point of I[01] holds [x,1] in IBB
proof
let x be Point of I[01];
x <= 1 by BORSUK_1:43;
then 2 * x <= 2 * 1 by XREAL_1:64;
then
A1: 1 is Point of I[01] & 2 * x - 1 <= 2 * 1 - 1 by BORSUK_1:43,XREAL_1:13;
x >= 0 by BORSUK_1:43;
then 1 - 2 * x <= 1 - 2 * 0 by XREAL_1:13;
hence thesis by A1,Def9;
end;
theorem Th66:
[1/2,0] in ICC & [1,1] in ICC
proof
A1: 0 <= 2 * (1/2) - 1;
1/2 is Point of I[01] & 0 is Point of I[01] by BORSUK_1:43;
hence [1/2,0] in ICC by A1,Def10;
1 is Point of I[01] & 1 <= 2 * 1 - 1 by BORSUK_1:43;
hence thesis by Def10;
end;
theorem Th67:
[1/2,0] in IBB
proof
A1: 0 <= 1 - 2 * (1/2);
1/2 is Point of I[01] & 0 is Point of I[01] by BORSUK_1:43;
hence thesis by A1,Def9;
end;
theorem Th68:
for x being Point of I[01] holds [1,x] in ICC
proof
let x be Point of I[01];
1 is Point of I[01] & x <= 2 * 1 - 1 by BORSUK_1:43;
hence thesis by Def10;
end;
theorem Th69:
for x being Point of I[01] st x >= 1/2 holds [x,0] in ICC
proof
let x be Point of I[01];
assume x >= 1/2;
then 2 * x >= 2 * (1/2) by XREAL_1:64;
then
A1: 2 * x - 1 >= 2 * (1/2) - 1 by XREAL_1:13;
0 is Point of I[01] by BORSUK_1:43;
hence thesis by A1,Def10;
end;
theorem Th70:
for x being Point of I[01] st x <= 1/2 holds [x,0] in IAA
proof
let x be Point of I[01];
assume x <= 1/2;
then 2 * x <= 2 * (1/2) by XREAL_1:64;
then
A1: 1 - 2 * x >= 1 - 2 * (1/2) by XREAL_1:13;
0 is Point of I[01] by BORSUK_1:43;
hence thesis by A1,Def8;
end;
theorem Th71:
for x being Point of I[01] st x < 1/2 holds not [x,0] in IBB &
not [x,0] in ICC
proof
let x be Point of I[01];
assume
A1: x < 1/2;
thus not [x,0] in IBB
proof
assume [x,0] in IBB;
then consider a, b being Point of I[01] such that
A2: [x,0] = [a,b] and
A3: b >= 1 - 2 * a and
b >= 2 * a - 1 by Def9;
x = a & b = 0 by A2,XTUPLE_0:1;
then 0 + 2 * x >= 1 by A3,XREAL_1:20;
then (2 * x)/2 >= 1/2 by XREAL_1:72;
hence thesis by A1;
end;
not [x,0] in ICC
proof
assume [x,0] in ICC;
then consider a, b being Point of I[01] such that
A4: [x,0] = [a,b] and
A5: b <= 2 * a - 1 by Def10;
x = a & b = 0 by A4,XTUPLE_0:1;
then 0 + 1 <= 2 * x by A5,XREAL_1:19;
then 1/2 <= (2 * x)/2 by XREAL_1:72;
hence thesis by A1;
end;
hence thesis;
end;
theorem Th72:
IAA /\ ICC = { [1/2,0] }
proof
thus IAA /\ ICC c= { [1/2,0] }
proof
let x be object;
assume
A1: x in IAA /\ ICC;
then reconsider y = x as Point of [:I[01], I[01]:];
x in IAA by A1,XBOOLE_0:def 4;
then
A2: y`1 <= 1/2 by Th59;
A3: x in ICC by A1,XBOOLE_0:def 4;
then y`1 >= 1/2 by Th60;
then
A4: y`1 = 1/2 by A2,XXREAL_0:1;
y in the carrier of [:I[01], I[01]:];
then
A5: y in [:the carrier of I[01], the carrier of I[01]:] by BORSUK_1:def 2;
A6: y`2 is Point of I[01] by Th27;
ex q being Point of [:I[01], I[01]:] st q = y & q`2 <= 2 * (q`1) - 1 by A3
,Th55;
then y`2 = 0 by A4,A6,BORSUK_1:43;
then y = [1/2,0] by A5,A4,MCART_1:21;
hence thesis by TARSKI:def 1;
end;
1/2 is Point of I[01] by BORSUK_1:43;
then [1/2,0] in IAA & [1/2,0] in ICC by Th69,Th70;
then [1/2,0] in IAA /\ ICC by XBOOLE_0:def 4;
hence thesis by ZFMISC_1:31;
end;
Lm1: for x, y being Point of I[01] holds [x,y] in the carrier of [:I[01],
I[01]:];
begin :: Properties of a Homotopy
reserve X for non empty pathwise_connected TopSpace,
a1, b1, c1, d1 for Point of X;
theorem Th73:
for P be Path of a, b, Q be Path of b, c, R be Path of c, d st a
,b are_connected & b,c are_connected & c,d are_connected holds (P + Q) + R, P +
(Q + R) are_homotopic
proof
let P be Path of a, b, Q be Path of b, c, R be Path of c, d such that
A1: a,b are_connected & b,c are_connected and
A2: c,d are_connected;
a,c are_connected & RePar (P + Q + R, 3RP) = P + (Q + R) by A1,A2,Th42,Th52;
hence thesis by A2,Th42,Th45,Th49;
end;
theorem
for P be Path of a1, b1, Q be Path of b1, c1, R be Path of c1, d1
holds (P + Q) + R, P + (Q + R) are_homotopic
proof
let P be Path of a1, b1, Q be Path of b1, c1, R be Path of c1, d1;
A1: c1,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,Th73;
end;
theorem Th75:
for P1, P2 being Path of a, b, Q1, Q2 being Path of b, c st a, b
are_connected & b, c are_connected & P1, P2 are_homotopic & Q1, Q2
are_homotopic holds P1 + Q1, P2 + Q2 are_homotopic
proof
set BB = [:I[01],I[01]:];
reconsider R1 = L[01](0,1/2,0,1) as continuous Function of
Closed-Interval-TSpace(0,1/2), I[01] by Th34,TOPMETR:20;
let P1, P2 be Path of a, b, Q1, Q2 be Path of b, c;
assume that
A1: a,b are_connected & b,c are_connected and
A2: P1,P2 are_homotopic and
A3: Q1,Q2 are_homotopic;
reconsider R2 = L[01](1/2,1,0,1) as continuous Function of
Closed-Interval-TSpace(1/2,1), I[01] by Th34,TOPMETR:20;
A4: 1 is Point of I[01] by BORSUK_1:43;
A5: 0 is Point of I[01] by BORSUK_1:43;
then reconsider A01 = [.0,1.] as non empty Subset of I[01] by A4,BORSUK_4:24;
A6: 1/2 is Point of I[01] by BORSUK_1:43;
then reconsider B01 = [.0,1/2.] as non empty Subset of I[01] by A5,
BORSUK_4:24;
reconsider N2 = [:[.1/2,1.], [.0,1.]:] as compact non empty Subset of BB by
A5,A4,A6,Th9;
reconsider N1 = [:[.0,1/2.], [.0,1.]:] as compact non empty Subset of BB by
A5,A4,A6,Th9;
set T1 = BB | N1;
set T2 = BB | N2;
A01 = [#] I[01] by BORSUK_1:40;
then
A7: I[01] = I[01] | A01 by TSEP_1:93;
set f1 = [:R1,id I[01]:], g1 = [:R2,id I[01]:];
reconsider f1 as continuous Function of [:Closed-Interval-TSpace(0,1/2),
I[01]:], [:I[01],I[01]:];
reconsider g1 as continuous Function of [:Closed-Interval-TSpace(1/2,1),
I[01]:], [:I[01],I[01]:];
A8: dom g1 = the carrier of [:Closed-Interval-TSpace(1/2,1), I[01]:] by
FUNCT_2:def 1
.= [:the carrier of Closed-Interval-TSpace(1/2,1), the carrier of I[01]
:] by BORSUK_1:def 2;
reconsider B02 = [.1/2,1.] as non empty Subset of I[01] by A4,A6,BORSUK_4:24;
consider f being Function of [:I[01],I[01]:], T such that
A9: f is continuous and
A10: for s being Point of I[01] holds f.(s,0) = P1.s & f.(s,1) = P2.s &
for t being Point of I[01] holds f.(0,t) = a & f.(1,t) = b by A2;
Closed-Interval-TSpace (0,1/2) = I[01] | B01 by TOPMETR:24;
then T1 = [:Closed-Interval-TSpace(0,1/2),I[01]:] by A7,BORSUK_3:22;
then reconsider K1 = f * f1 as continuous Function of T1, T by A9;
consider g being Function of [:I[01],I[01]:], T such that
A11: g is continuous and
A12: for s being Point of I[01] holds g.(s,0) = Q1.s & g.(s,1) = Q2.s &
for t being Point of I[01] holds g.(0,t) = b & g.(1,t) = c by A3;
Closed-Interval-TSpace (1/2,1) = I[01] | B02 by TOPMETR:24;
then T2 = [:Closed-Interval-TSpace(1/2,1),I[01]:] by A7,BORSUK_3:22;
then reconsider K2 = g * g1 as continuous Function of T2, T by A11;
A13: dom K2 = the carrier of [:Closed-Interval-TSpace(1/2,1), I[01]:] by
FUNCT_2:def 1
.= [:the carrier of Closed-Interval-TSpace(1/2,1), the carrier of I[01]
:] by BORSUK_1:def 2;
A14: for p be set st p in ([#] T1) /\ ([#] T2) holds K1.p = K2.p
proof
A15: R2. (1/2) = 0 by Th33;
let p be set;
A16: R1. (1/2) = 1 by Th33;
assume p in ([#] T1) /\ ([#] T2);
then p in [:{1/2}, [.0,1.] :] by Th29;
then consider x, y being object such that
A17: x in {1/2} and
A18: y in [.0,1.] and
A19: p = [x,y] by ZFMISC_1:def 2;
A20: y in the carrier of I[01] by A18,TOPMETR:18,20;
reconsider y as Point of I[01] by A18,TOPMETR:18,20;
A21: x = 1/2 by A17,TARSKI:def 1;
then x in [.1/2,1.] by XXREAL_1:1;
then
A22: x in the carrier of Closed-Interval-TSpace(1/2,1) by TOPMETR:18;
then p in [:the carrier of Closed-Interval-TSpace(1/2,1), the carrier of
I[01]:] by A19,A20,ZFMISC_1:87;
then p in the carrier of [:Closed-Interval-TSpace(1/2,1),I[01]:] by
BORSUK_1:def 2;
then
A23: p in dom g1 by FUNCT_2:def 1;
x in [.0,1/2.] by A21,XXREAL_1:1;
then
A24: x in the carrier of Closed-Interval-TSpace(0,1/2) by TOPMETR:18;
then x in dom R1 by FUNCT_2:def 1;
then
A25: [x,y] in [:dom R1, dom id I[01]:] by ZFMISC_1:87;
x in dom R2 by A22,FUNCT_2:def 1;
then
A26: [x,y] in [:dom R2, dom id I[01]:] by ZFMISC_1:87;
p in [:the carrier of Closed-Interval-TSpace(0,1/2), the carrier of
I[01]:] by A19,A20,A24,ZFMISC_1:87;
then p in the carrier of [:Closed-Interval-TSpace(0,1/2),I[01]:] by
BORSUK_1:def 2;
then p in dom f1 by FUNCT_2:def 1;
then K1.p = f.(f1.(x,y)) by A19,FUNCT_1:13
.= f.(R1.x,(id I[01]).y) by A25,FUNCT_3:65
.= b by A10,A21,A16
.= g.(R2.x,(id I[01]).y) by A12,A21,A15
.= g.(g1.(x,y)) by A26,FUNCT_3:65
.= K2.p by A19,A23,FUNCT_1:13;
hence thesis;
end;
([#] T1) \/ ([#] T2) = [#] BB by Th28;
then consider h being Function of [:I[01],I[01]:], T such that
A27: h = K1 +* K2 and
A28: h is continuous by A14,BORSUK_2:1;
A29: dom f1 = the carrier of [:Closed-Interval-TSpace(0,1/2), I[01]:] by
FUNCT_2:def 1
.= [:the carrier of Closed-Interval-TSpace(0,1/2), the carrier of I[01]
:] by BORSUK_1:def 2;
A30: for s being Point of I[01] holds h.(s,0) = (P1+Q1).s & h.(s,1) = (P2+Q2
).s
proof
let s be Point of I[01];
A31: h.(s,1) = (P2+Q2).s
proof
per cases;
suppose
A32: s < 1/2;
then
A33: 2 * s is Point of I[01] by Th3;
A34: 1 in the carrier of I[01] by BORSUK_1:43;
then
A35: 1 in dom id I[01];
A36: s >= 0 by BORSUK_1:43;
then
A37: R1.s = ((1 - 0)/(1/2 - 0)) * (s - 0) + 0 by A32,Th35
.= 2 * s;
s in [.0,1/2.] by A32,A36,XXREAL_1:1;
then
A38: s in the carrier of Closed-Interval-TSpace(0,1/2) by TOPMETR:18;
then
A39: [s,1] in dom f1 by A29,A34,ZFMISC_1:87;
s in dom R1 by A38,FUNCT_2:def 1;
then
A40: [s,1] in [:dom R1, dom id I[01]:] by A35,ZFMISC_1:87;
not s in [.1/2,1.] by A32,XXREAL_1:1;
then not s in the carrier of Closed-Interval-TSpace(1/2,1) by
TOPMETR:18;
then not [s,1] in dom K2 by A13,ZFMISC_1:87;
then h.(s,1) = K1.(s,1) by A27,FUNCT_4:11
.= f.(f1.(s,1)) by A39,FUNCT_1:13
.= f.(R1.s,(id I[01]).1) by A40,FUNCT_3:65
.= f.(2*s,1) by A4,A37,FUNCT_1:18
.= P2.(2 * s) by A10,A33;
hence thesis by A1,A32,BORSUK_2:def 5;
end;
suppose
A41: s >= 1/2;
A42: s <= 1 by BORSUK_1:43;
then
A43: R2.s = ((1 - 0)/(1 - 1/2)) * (s - 1/2) + 0 by A41,Th35
.= 2 * s - 1;
A44: 2 * s - 1 is Point of I[01] by A41,Th4;
A45: 1 in the carrier of I[01] by BORSUK_1:43;
then
A46: 1 in dom id I[01];
s in [.1/2,1.] by A41,A42,XXREAL_1:1;
then
A47: s in the carrier of Closed-Interval-TSpace(1/2,1) by TOPMETR:18;
then
A48: [s,1] in dom g1 by A8,A45,ZFMISC_1:87;
s in dom R2 by A47,FUNCT_2:def 1;
then
A49: [s,1] in [:dom R2, dom id I[01]:] by A46,ZFMISC_1:87;
[s,1] in dom K2 by A13,A47,A45,ZFMISC_1:87;
then h.(s,1) = K2.(s,1) by A27,FUNCT_4:13
.= g.(g1.(s,1)) by A48,FUNCT_1:13
.= g.(R2.s,(id I[01]).1) by A49,FUNCT_3:65
.= g.(2*s-1,1) by A4,A43,FUNCT_1:18
.= Q2.(2 * s - 1) by A12,A44;
hence thesis by A1,A41,BORSUK_2:def 5;
end;
end;
h.(s,0) = (P1+Q1).s
proof
per cases;
suppose
A50: s < 1/2;
then
A51: 2 * s is Point of I[01] by Th3;
A52: 0 in the carrier of I[01] by BORSUK_1:43;
then
A53: 0 in dom id I[01];
A54: s >= 0 by BORSUK_1:43;
then
A55: R1.s = ((1 - 0)/(1/2 - 0)) * (s - 0) + 0 by A50,Th35
.= 2 * s;
s in [.0,1/2.] by A50,A54,XXREAL_1:1;
then
A56: s in the carrier of Closed-Interval-TSpace(0,1/2) by TOPMETR:18;
then
A57: [s,0] in dom f1 by A29,A52,ZFMISC_1:87;
s in dom R1 by A56,FUNCT_2:def 1;
then
A58: [s,0] in [:dom R1, dom id I[01]:] by A53,ZFMISC_1:87;
not s in [.1/2,1.] by A50,XXREAL_1:1;
then not s in the carrier of Closed-Interval-TSpace(1/2,1) by
TOPMETR:18;
then not [s,0] in dom K2 by A13,ZFMISC_1:87;
then h.(s,0) = K1.(s,0) by A27,FUNCT_4:11
.= f.(f1.(s,0)) by A57,FUNCT_1:13
.= f.(R1.s,(id I[01]).0) by A58,FUNCT_3:65
.= f.(2*s,0) by A5,A55,FUNCT_1:18
.= P1.(2 * s) by A10,A51;
hence thesis by A1,A50,BORSUK_2:def 5;
end;
suppose
A59: s >= 1/2;
A60: s <= 1 by BORSUK_1:43;
then
A61: R2.s = ((1 - 0)/(1 - 1/2)) * (s - 1/2) + 0 by A59,Th35
.= 2 * s - 1;
A62: 2 * s - 1 is Point of I[01] by A59,Th4;
A63: 0 in the carrier of I[01] by BORSUK_1:43;
then
A64: 0 in dom id I[01];
s in [.1/2,1.] by A59,A60,XXREAL_1:1;
then
A65: s in the carrier of Closed-Interval-TSpace(1/2,1) by TOPMETR:18;
then
A66: [s,0] in dom g1 by A8,A63,ZFMISC_1:87;
s in dom R2 by A65,FUNCT_2:def 1;
then
A67: [s,0] in [:dom R2, dom id I[01]:] by A64,ZFMISC_1:87;
[s,0] in dom K2 by A13,A65,A63,ZFMISC_1:87;
then h.(s,0) = K2.(s,0) by A27,FUNCT_4:13
.= g.(g1.(s,0)) by A66,FUNCT_1:13
.= g.(R2.s,(id I[01]).0) by A67,FUNCT_3:65
.= g.(2*s-1,0) by A5,A61,FUNCT_1:18
.= Q1.(2 * s - 1) by A12,A62;
hence thesis by A1,A59,BORSUK_2:def 5;
end;
end;
hence thesis by A31;
end;
take h;
for t being Point of I[01] holds h.(0,t) = a & h.(1,t) = c
proof
let t be Point of I[01];
A68: dom K2 = the carrier of [:Closed-Interval-TSpace(1/2,1), I[01]:] by
FUNCT_2:def 1
.= [:the carrier of Closed-Interval-TSpace(1/2,1), the carrier of
I[01]:] by BORSUK_1:def 2;
0 in [.0,1/2.] by XXREAL_1:1;
then
A69: 0 in the carrier of Closed-Interval-TSpace (0,1/2) by TOPMETR:18;
then
A70: [0,t] in dom f1 by A29,ZFMISC_1:87;
0 in dom R1 by A69,FUNCT_2:def 1;
then
A71: [0,t] in [:dom R1, dom id I[01]:] by ZFMISC_1:87;
not 0 in [.1/2,1.] by XXREAL_1:1;
then not 0 in the carrier of Closed-Interval-TSpace(1/2,1) by TOPMETR:18;
then not [0,t] in dom K2 by A68,ZFMISC_1:87;
hence h.(0,t) = K1.(0,t) by A27,FUNCT_4:11
.= f.(f1.(0,t)) by A70,FUNCT_1:13
.= f.(R1.0,(id I[01]).t) by A71,FUNCT_3:65
.= f.(R1.0,t) by FUNCT_1:18
.= f.(0,t) by Th33
.= a by A10;
1 in [.1/2,1.] by XXREAL_1:1;
then
A72: 1 in the carrier of Closed-Interval-TSpace (1/2,1) by TOPMETR:18;
then 1 in dom R2 by FUNCT_2:def 1;
then
A73: [1,t] in [:dom R2, dom id I[01]:] by ZFMISC_1:87;
1 in [.1/2,1.] by XXREAL_1:1;
then 1 in the carrier of Closed-Interval-TSpace (1/2,1) by TOPMETR:18;
then
A74: [1,t] in dom g1 by A8,ZFMISC_1:87;
[1,t] in dom K2 by A68,A72,ZFMISC_1:87;
then h.(1,t) = K2.(1,t) by A27,FUNCT_4:13
.= g.(g1.(1,t)) by A74,FUNCT_1:13
.= g.(R2.1,(id I[01]).t) by A73,FUNCT_3:65
.= g.(R2.1,t) by FUNCT_1:18
.= g.(1,t) by Th33
.= c by A12;
hence thesis;
end;
hence thesis by A28,A30;
end;
theorem
for P1, P2 being Path of a1, b1, Q1, Q2 being Path of b1, c1 st P1, P2
are_homotopic & Q1, Q2 are_homotopic holds P1 + Q1, P2 + Q2 are_homotopic
proof
let P1, P2 be Path of a1, b1, Q1, Q2 be Path of b1, c1;
a1, b1 are_connected & b1, c1 are_connected by BORSUK_2:def 3;
hence thesis by Th75;
end;
theorem Th77:
for P, Q being Path of a, b st a, b are_connected & P, Q
are_homotopic holds -P, -Q are_homotopic
proof
reconsider fF = id I[01] as continuous Function of I[01], I[01];
reconsider fB = L[01]((0,1)(#),(#)(0,1)) as continuous Function of I[01],
I[01] by TOPMETR:20,TREAL_1:8;
let P, Q be Path of a, b;
assume
A1: a,b are_connected;
set F = [:fB, fF:];
A2: dom fB = the carrier of I[01] by FUNCT_2:def 1;
assume P, Q are_homotopic;
then consider f being Function of [:I[01],I[01]:], T such that
A3: f is continuous and
A4: for s being Point of I[01] holds f.(s,0) = P.s & f.(s,1) = Q.s & for
t being Point of I[01] holds f.(0,t) = a & f.(1,t) = b;
reconsider ff = f * F as Function of [:I[01],I[01]:], T;
take ff;
thus ff is continuous by A3;
A5: 0 is Point of I[01] by BORSUK_1:43;
A6: for t being Point of I[01] holds ff.(0,t) = b & ff.(1,t) = a
proof
A7: for t being Point of I[01], t9 being Real
st t = t9 holds fB.t = 1-t9
proof
let t be Point of I[01], t9 be Real;
assume
A8: t = t9;
reconsider ee = t as Point of Closed-Interval-TSpace (0,1) by TOPMETR:20;
A9: (0,1)(#) = 1 & (#)(0,1) = 0 by TREAL_1:def 1,def 2;
fB.t = fB.ee .= ((0-1)*t9 + 1) by A8,A9,TREAL_1:7
.= (1 - 1*t9);
hence thesis;
end;
then
A10: fB.0 = 1 - 0 by A5
.= 1;
1 is Point of I[01] by BORSUK_1:43;
then
A11: fB.1 = 1 - 1 by A7
.= 0;
let t be Point of I[01];
A12: dom fF = the carrier of I[01];
reconsider tt = t as Real;
A13: dom fB = the carrier of I[01] by FUNCT_2:def 1;
then
A14: 0 in dom fB by BORSUK_1:43;
A15: dom F = [:dom fB, dom fF:] by FUNCT_3:def 8;
then
A16: [0,t] in dom F by A14,ZFMISC_1:87;
A17: 1 in dom fB by A13,BORSUK_1:43;
then
A18: [1,t] in dom F by A15,ZFMISC_1:87;
F.(1,t) = [fB.1,fF.t] by A12,A17,FUNCT_3:def 8
.= [0,tt] by A11,FUNCT_1:18;
then
A19: ff.(1,t) = f.(0,t) by A18,FUNCT_1:13
.= a by A4;
F.(0,t) = [fB.0,fF.t] by A12,A14,FUNCT_3:def 8
.= [1,tt] by A10,FUNCT_1:18;
then ff.(0,t) = f.(1,t) by A16,FUNCT_1:13
.= b by A4;
hence thesis by A19;
end;
for s being Point of I[01] holds ff.(s,0) = (-P).s & ff.(s,1) = (-Q).s
proof
let s be Point of I[01];
A20: for t being Point of I[01], t9 being Real st t = t9 holds fB.t = 1-t9
proof
let t be Point of I[01], t9 be Real;
assume
A21: t = t9;
reconsider ee = t as Point of Closed-Interval-TSpace (0,1) by TOPMETR:20;
A22: (0,1)(#) = 1 & (#)(0,1) = 0 by TREAL_1:def 1,def 2;
fB.t = fB.ee .= ((0-1)*t9 + 1) by A21,A22,TREAL_1:7
.= (1 - 1*t9);
hence thesis;
end;
A23: fB.s = 1 - s by A20;
A24: 1 is Point of I[01] by BORSUK_1:43;
A25: dom F = [:dom fB, dom fF:] by FUNCT_3:def 8;
A26: 1 in dom fF by BORSUK_1:43;
then
A27: [s,1] in dom F by A2,A25,ZFMISC_1:87;
A28: 0 in dom fF by BORSUK_1:43;
then
A29: [s,0] in dom F by A2,A25,ZFMISC_1:87;
A30: 1-s is Point of I[01] by JORDAN5B:4;
F.(s,1) = [fB.s,fF.1] by A2,A26,FUNCT_3:def 8
.= [1-s,1] by A23,A24,FUNCT_1:18;
then
A31: ff.(s,1) = f.(1-s,1) by A27,FUNCT_1:13
.= Q.(1-s) by A4,A30
.= (-Q).s by A1,BORSUK_2:def 6;
F.(s,0) = [fB.s,fF.0] by A2,A28,FUNCT_3:def 8
.= [1-s, 0] by A5,A23,FUNCT_1:18;
then ff.(s,0) = f.(1-s,0) by A29,FUNCT_1:13
.= P.(1-s) by A4,A30
.= (-P).s by A1,BORSUK_2:def 6;
hence thesis by A31;
end;
hence thesis by A6;
end;
theorem
for P, Q being Path of a1, b1 st P, Q are_homotopic holds -P, -Q
are_homotopic by Th77,BORSUK_2:def 3;
theorem
for P, Q, R be Path of a, b holds P, Q are_homotopic & Q, R
are_homotopic implies P, R are_homotopic
proof
1/2 in [.0,1/2.] by XXREAL_1:1;
then
A1: 1/2 in the carrier of Closed-Interval-TSpace(0,1/2) by TOPMETR:18;
reconsider B02 = [.1/2,1.] as non empty Subset of I[01] by BORSUK_1:40
,XXREAL_1:1,34;
A2: 1 in [.0,1.] by XXREAL_1:1;
A3: 1/2 in [.1/2,1.] by XXREAL_1:1;
then
A4: 1/2 in the carrier of Closed-Interval-TSpace(1/2,1) by TOPMETR:18;
[.0,1/2.] c= the carrier of I[01] by BORSUK_1:40,XXREAL_1:34;
then
A5: [:[.0,1.], [.0,1/2.]:] c= [:the carrier of I[01], the carrier of I[01]
:] by BORSUK_1:40,ZFMISC_1:96;
A6: the carrier of Closed-Interval-TSpace(0,1/2) = [. 0,1/2 .] by TOPMETR:18;
0 in [.0,1/2.] by XXREAL_1:1;
then reconsider Ewa = [:[.0,1.], [.0,1/2.]:] as non empty Subset of [:I[01],
I[01]:] by A5,A2,BORSUK_1:def 2;
set T1 = [:I[01], I[01]:] | Ewa;
reconsider P2 = P[01](1/2, 1, (#)(0,1), (0,1)(#)) as continuous Function of
Closed-Interval-TSpace(1/2,1), I[01] by TOPMETR:20,TREAL_1:12;
reconsider P1 = P[01](0, 1/2, (#)(0,1), (0,1)(#)) as continuous Function of
Closed-Interval-TSpace(0,1/2), I[01] by TOPMETR:20,TREAL_1:12;
let P, Q, R be Path of a, b;
assume that
A7: P, Q are_homotopic and
A8: Q, R are_homotopic;
consider f being Function of [:I[01],I[01]:], T such that
A9: f is continuous and
A10: for s being Point of I[01] holds f.(s,0) = P.s & f.(s,1) = Q.s & for
t being Point of I[01] holds f.(0,t) = a & f.(1,t) = b by A7;
A11: the carrier of Closed-Interval-TSpace(1/2,1) = [. 1/2,1 .] by TOPMETR:18;
[.0,1.] c= the carrier of I[01] by BORSUK_1:40;
then reconsider A01 = [.0,1.] as non empty Subset of I[01] by XXREAL_1:1;
reconsider B01 = [.0,1/2.] as non empty Subset of I[01] by BORSUK_1:40
,XXREAL_1:1,34;
A12: the carrier of Closed-Interval-TSpace(1/2,1) = [.1/2,1.] by TOPMETR:18;
A01 = [#] I[01] by BORSUK_1:40;
then
A13: I[01] = I[01] | A01 by TSEP_1:93;
[.1/2,1.] c= the carrier of I[01] by BORSUK_1:40,XXREAL_1:34;
then
A14: [:[.0,1.], [.1/2,1.]:] c= [:the carrier of I[01], the carrier of I[01]
:] by BORSUK_1:40,ZFMISC_1:96;
A15: 1 in the carrier of I[01] by BORSUK_1:43;
1 in [.1/2,1.] by XXREAL_1:1;
then reconsider
Ewa1 = [:[.0,1.], [.1/2,1.]:] as non empty Subset of [:I[01],
I[01]:] by A2,A14,BORSUK_1:def 2;
set T2 = [:I[01], I[01]:] | Ewa1;
set e1 = [:id I[01], P1:], e2 = [:id I[01], P2:];
A16: dom id I[01] = the carrier of I[01] & dom P[01](1/2, 1, (#)(0,1), (0,1)
(#)) = the carrier of Closed-Interval-TSpace(1/2, 1) by FUNCT_2:def 1;
A17: rng e2 = [:rng id I[01], rng P[01](1/2, 1, (#)(0,1), (0,1)(#)):] by
FUNCT_3:67;
consider g being Function of [:I[01],I[01]:], T such that
A18: g is continuous and
A19: for s being Point of I[01] holds g.(s,0) = Q.s & g.(s,1) = R.s & for
t being Point of I[01] holds g.(0,t) = a & g.(1,t) = b by A8;
set f1 = f * e1, g1 = g * e2;
dom g = the carrier of [:I[01], I[01]:] by FUNCT_2:def 1
.= [:the carrier of I[01], the carrier of I[01]:] by BORSUK_1:def 2;
then
A20: dom g1 = dom e2 by A17,RELAT_1:27,TOPMETR:20,ZFMISC_1:96
.= [:the carrier of I[01], the carrier of Closed-Interval-TSpace(1/2,1)
:] by A16,FUNCT_3:def 8;
Closed-Interval-TSpace (1/2,1) = I[01] | B02 by TOPMETR:24;
then e2 is continuous Function of [:I[01],Closed-Interval-TSpace(1/2,1):],
[:I[01] ,I[01]:] & T2 = [:I[01],Closed-Interval-TSpace(1/2,1):] by A13,
BORSUK_3:22;
then reconsider g1 as continuous Function of T2,T by A18;
Closed-Interval-TSpace (0,1/2) = I[01] | B01 by TOPMETR:24;
then e1 is continuous Function of [:I[01],Closed-Interval-TSpace(0,1/2):],
[:I[01] ,I[01]:] & T1 = [:I[01],Closed-Interval-TSpace(0,1/2):] by A13,
BORSUK_3:22;
then reconsider f1 as continuous Function of T1, T by A9;
A21: 1 is Point of I[01] by BORSUK_1:43;
A22: 0 is Point of I[01] by BORSUK_1:43;
then
A23: [.0,1.] is compact Subset of I[01] by A21,BORSUK_4:24;
A24: 1/2 is Point of I[01] by BORSUK_1:43;
then [.0,1/2.] is compact Subset of I[01] by A22,BORSUK_4:24;
then
A25: Ewa is compact Subset of [:I[01], I[01]:] by A23,BORSUK_3:23;
[.1/2,1.] is compact Subset of I[01] by A21,A24,BORSUK_4:24;
then
A26: Ewa1 is compact Subset of [:I[01], I[01]:] by A23,BORSUK_3:23;
A27: dom e1 = the carrier of [:I[01], Closed-Interval-TSpace(0,1/2):] by
FUNCT_2:def 1
.= [:the carrier of I[01], the carrier of Closed-Interval-TSpace(0,1/2)
:] by BORSUK_1:def 2;
A28: dom e2 = [:dom id I[01], dom P2:] by FUNCT_3:def 8;
A29: dom e1 = [:dom id I[01], dom P1:] by FUNCT_3:def 8;
A30: dom e2 = the carrier of [:I[01], Closed-Interval-TSpace(1/2,1):] by
FUNCT_2:def 1
.= [:the carrier of I[01], the carrier of Closed-Interval-TSpace(1/2,1)
:] by BORSUK_1:def 2;
A31: [#] T1 = Ewa & [#] T2 = Ewa1 by PRE_TOPC:def 5;
then
A32: [#] T1 /\ [#] T2 = [:[.0,1.], [.0,1/2.] /\ [.1/2,1.]:] by ZFMISC_1:99
.= [:[.0,1.], {1/2} :] by XXREAL_1:418;
A33: for p be set st p in [#] T1 /\ [#] T2 holds f1.p = g1.p
proof
let p be set;
assume p in [#] T1 /\ [#] T2;
then consider x, y be object such that
A34: x in [.0,1.] and
A35: y in {1/2} and
A36: p = [x,y] by A32,ZFMISC_1:def 2;
x in { r where r is Real: 0 <= r & r <= 1 } by A34,RCOMP_1:def 1;
then
A37: ex r1 be Real st r1 = x & 0 <= r1 & r1 <= 1;
then reconsider x9 = x as Point of I[01] by BORSUK_1:43;
A38: y = 1/2 by A35,TARSKI:def 1;
f1.p = g1.p
proof
1/2 in [.0,1/2.] by XXREAL_1:1;
then reconsider y9 = 1/2 as Point of Closed-Interval-TSpace(0,1/2) by
TOPMETR:18;
set t9 = 1/2;
reconsider r1 = (#)(0,1), r2 = (0,1)(#) as Real;
A39: P1.y9 = ((r2 - r1)/(1/2 - 0))*t9 + ((1/2)*r1 - 0 *r2)/(1/2 - 0) by
TREAL_1:11
.= ((1 - r1)/(1/2 - 0))*t9 + ((1/2)*r1 - 0 *r2)/(1/2 - 0) by
TREAL_1:def 2
.= ((1 - 0)/(1/2 - 0))*t9 + ((1/2)*r1 - 0 *r2)/(1/2 - 0) by
TREAL_1:def 1
.= ((1 - 0)/(1/2 - 0))*t9 + ((1/2)*0 - 0 *1)/(1/2 - 0) by TREAL_1:def 1
.= 1;
reconsider y9 = 1/2 as Point of Closed-Interval-TSpace(1/2,1) by A3,
TOPMETR:18;
A40: P2.y9 = ((r2 - r1)/(1 - 1/2))*t9 + (1*r1 - (1/2)*r2)/(1 - 1/2) by
TREAL_1:11
.= 0 by BORSUK_1:def 14,TREAL_1:5;
A41: x in the carrier of I[01] by A37,BORSUK_1:43;
then
A42: [x,y] in dom e2 by A30,A4,A38,ZFMISC_1:87;
A43: [x,y] in dom e1 by A1,A27,A38,A41,ZFMISC_1:87;
then f1.p = f.(e1.(x,y)) by A36,FUNCT_1:13
.= f.(id I[01].x, P1.y) by A29,A43,FUNCT_3:65
.= f.(x9,1) by A38,A39,FUNCT_1:18
.= Q.x9 by A10
.= g.(x9,0) by A19
.= g.(id I[01]. x9, P2.y) by A38,A40,FUNCT_1:18
.= g.(e2.(x, y)) by A28,A42,FUNCT_3:65
.= g1. p by A36,A42,FUNCT_1:13;
hence thesis;
end;
hence thesis;
end;
[#] T1 \/ [#] T2 = [:[.0,1.], [.0,1/2.] \/ [.1/2,1.]:] by A31,ZFMISC_1:97
.= [:the carrier of I[01], the carrier of I[01]:] by BORSUK_1:40
,XXREAL_1:174
.= [#] [:I[01],I[01]:] by BORSUK_1:def 2;
then consider h being Function of [:I[01],I[01]:], T such that
A44: h = f1 +* g1 and
A45: h is continuous by A25,A26,A33,BORSUK_2:1;
A46: the carrier of Closed-Interval-TSpace(0,1/2) = [.0,1/2.] by TOPMETR:18;
A47: for t being Point of I[01] holds h.(0,t) = a & h.(1,t) = b
proof
let t be Point of I[01];
per cases;
suppose
A48: t < 1/2;
reconsider r1 = (#)(0,1), r2 = (0,1)(#) as Real;
A49: 0 <= t by BORSUK_1:43;
then
A50: t in the carrier of Closed-Interval-TSpace(0,1/2) by A6,A48,XXREAL_1:1;
0 in the carrier of I[01] by BORSUK_1:43;
then
A51: [0,t] in dom e1 by A27,A50,ZFMISC_1:87;
P1.t = ((r2 - r1)/(1/2 - 0))*t + ((1/2)*r1 - 0 *r2)/(1/2 - 0) by A50,
TREAL_1:11
.= ((1 - r1)/(1/2))*t + ((1/2)*r1)/(1/2) by TREAL_1:def 2
.= ((1 - 0)/(1/2))*t + ((1/2)*r1)/(1/2) by TREAL_1:def 1
.= (1/(1/2))*t + ((1/2)*0)/(1/2) by TREAL_1:def 1
.= 2*t;
then
A52: P1.t is Point of I[01] by A48,Th3;
not t in the carrier of Closed-Interval-TSpace(1/2,1) by A11,A48,
XXREAL_1:1;
then not [0,t] in dom g1 by A20,ZFMISC_1:87;
hence h.(0,t) = f1.(0,t) by A44,FUNCT_4:11
.= f.(e1.(0,t)) by A51,FUNCT_1:13
.= f.(id I[01].0, P1.t) by A29,A51,FUNCT_3:65
.= f.(0,P1.t) by A22,FUNCT_1:18
.= a by A10,A52;
t in the carrier of Closed-Interval-TSpace(0,1/2) by A46,A48,A49,
XXREAL_1:1;
then
A53: [1,t] in dom e1 by A27,A15,ZFMISC_1:87;
P1.t = ((r2 - r1)/(1/2 - 0))*t + ((1/2)*r1 - 0 *r2)/(1/2 - 0) by A50,
TREAL_1:11
.= ((1 - r1)/(1/2))*t + ((1/2)*r1)/(1/2) by TREAL_1:def 2
.= ((1 - 0)/(1/2))*t + ((1/2)*r1)/(1/2) by TREAL_1:def 1
.= (1/(1/2))*t + ((1/2)*0)/(1/2) by TREAL_1:def 1
.= 2*t;
then
A54: P1.t is Point of I[01] by A48,Th3;
not t in the carrier of Closed-Interval-TSpace(1/2,1) by A12,A48,
XXREAL_1:1;
then not [1,t] in dom g1 by A20,ZFMISC_1:87;
hence h.(1,t) = f1.(1,t) by A44,FUNCT_4:11
.= f.(e1.(1,t)) by A53,FUNCT_1:13
.= f.(id I[01]. 1, P1.t) by A29,A53,FUNCT_3:65
.= f.(1,P1.t) by A21,FUNCT_1:18
.= b by A10,A54;
end;
suppose
A55: t >= 1/2;
reconsider r1 = (#)(0,1), r2 = (0,1)(#) as Real;
t <= 1 by BORSUK_1:43;
then
A56: t in the carrier of Closed-Interval-TSpace(1/2,1) by A11,A55,XXREAL_1:1;
then
A57: [1,t] in dom e2 by A30,A15,ZFMISC_1:87;
P2.t = ((r2 - r1)/(1 - 1/2))*t + (1*r1 - (1/2) *r2)/(1 - 1/2) by A56,
TREAL_1:11
.= ((1 - r1)/(1/2))*t + (1*r1 - (1/2) *r2)/(1/2) by TREAL_1:def 2
.= ((1 - 0)/(1/2))*t + (1*r1 - (1/2) *r2)/(1/2) by TREAL_1:def 1
.= 2*t + (1*0 - (1/2) *r2)/(1/2) by TREAL_1:def 1
.= 2*t + (-(1/2) *r2)/(1/2)
.= 2*t + (-(1/2) *1)/(1/2) by TREAL_1:def 2
.= 2*t - 1;
then
A58: P2.t is Point of I[01] by A55,Th4;
P2.t = ((r2 - r1)/(1 - 1/2))*t + (1*r1 - (1/2) *r2)/(1 - 1/2) by A56,
TREAL_1:11
.= ((1 - r1)/(1/2))*t + (1*r1 - (1/2) *r2)/(1/2) by TREAL_1:def 2
.= ((1 - 0)/(1/2))*t + (1*r1 - (1/2) *r2)/(1/2) by TREAL_1:def 1
.= (1/(1/2))*t + (1*0 - (1/2) *r2)/(1/2) by TREAL_1:def 1
.= (1/(1/2))*t + (1*0 - (1/2) *1)/(1/2) by TREAL_1:def 2
.= 2*t - 1;
then
A59: P2.t is Point of I[01] by A55,Th4;
A60: 0 in the carrier of I[01] by BORSUK_1:43;
then
A61: [0,t] in dom e2 by A30,A56,ZFMISC_1:87;
[0,t] in dom g1 by A20,A60,A56,ZFMISC_1:87;
hence h.(0,t) = g1.(0,t) by A44,FUNCT_4:13
.= g.(e2.(0,t)) by A61,FUNCT_1:13
.= g.(id I[01]. 0, P2.t) by A28,A61,FUNCT_3:65
.= g.(0,P2.t) by A22,FUNCT_1:18
.= a by A19,A59;
[1,t] in dom g1 by A20,A15,A56,ZFMISC_1:87;
hence h.(1,t) = g1.(1,t) by A44,FUNCT_4:13
.= g.(e2.(1,t)) by A57,FUNCT_1:13
.= g.(id I[01]. 1, P2.t) by A28,A57,FUNCT_3:65
.= g.(1,P2.t) by A21,FUNCT_1:18
.= b by A19,A58;
end;
end;
for s being Point of I[01] holds h.(s,0) = P.s & h.(s,1) = R.s
proof
reconsider r1 = (#)(0,1), r2 = (0,1)(#) as Real;
let s be Point of I[01];
1 = (0,1)(#) & 1 = (1/2,1)(#) by TREAL_1:def 2;
then
A62: P2.1 = 1 by TREAL_1:13;
A63: the carrier of Closed-Interval-TSpace(1/2,1) = [. 1/2,1 .] by TOPMETR:18;
then
A64: 1 in the carrier of Closed-Interval-TSpace(1/2,1) by XXREAL_1:1;
then
A65: [s,1] in dom e2 by A30,ZFMISC_1:87;
[s,1] in dom g1 by A20,A64,ZFMISC_1:87;
then
A66: h.(s,1) = g1.(s,1) by A44,FUNCT_4:13
.= g.(e2.(s,1)) by A65,FUNCT_1:13
.= g.(id I[01]. s, P2.1) by A28,A65,FUNCT_3:65
.= g.(s,1) by A62,FUNCT_1:18
.= R.s by A19;
A67: 0 in the carrier of Closed-Interval-TSpace(0,1/2) by A6,XXREAL_1:1;
then
A68: P1.0 = ((r2 - r1)/(1/2 - 0))*0 + ((1/2)*r1 - 0 *r2)/(1/2 - 0) by
TREAL_1:11
.= ((1/2)*0 - 0 *r2)/(1/2 - 0)by TREAL_1:def 1;
A69: [s,0] in dom e1 by A27,A67,ZFMISC_1:87;
not 0 in the carrier of Closed-Interval-TSpace(1/2,1) by A63,XXREAL_1:1;
then not [s,0] in dom g1 by A20,ZFMISC_1:87;
then h.(s,0) = f1.(s,0) by A44,FUNCT_4:11
.= f.(e1.(s,0)) by A69,FUNCT_1:13
.= f.(id I[01].s, P1.0) by A29,A69,FUNCT_3:65
.= f.(s,0) by A68,FUNCT_1:18
.= P.s by A10;
hence thesis by A66;
end;
hence thesis by A45,A47;
end;
theorem Th80:
for P be Path of a, b, Q be constant Path of b, b st a, b
are_connected holds P + Q, P are_homotopic
proof
let P be Path of a, b, Q be constant Path of b, b such that
A1: a,b are_connected;
RePar (P, 1RP) = P + Q by A1,Th50;
hence thesis by A1,Th45,Th47;
end;
theorem
for P be Path of a1, b1, Q be constant Path of b1, b1 holds P + Q, P
are_homotopic by Th80,BORSUK_2:def 3;
theorem Th82:
for P be Path of a, b, Q be constant Path of a, a st a, b
are_connected holds Q + P, P are_homotopic
proof
let P be Path of a, b, Q be constant Path of a, a such that
A1: a,b are_connected;
RePar (P, 2RP) = Q + P by A1,Th51;
hence thesis by A1,Th45,Th48;
end;
theorem
for P be Path of a1, b1, Q be constant Path of a1, a1 holds Q + P, P
are_homotopic by Th82,BORSUK_2:def 3;
theorem Th84:
for P being Path of a, b, Q being constant Path of a, a st a, b
are_connected holds P + - P, Q are_homotopic
proof
set S = [:I[01],I[01]:];
let P be Path of a, b, Q be constant Path of a, a such that
A1: a, b are_connected;
reconsider e2 = pr2(the carrier of I[01], the carrier of I[01]) as
continuous Function of S, I[01] by YELLOW12:40;
set gg = (-P) * e2;
-P is continuous by A1,BORSUK_2:def 2;
then reconsider gg as continuous Function of S, T;
set S2 = S|IBB;
reconsider g = gg|IBB as Function of S2, T by PRE_TOPC:9;
reconsider g as continuous Function of S2, T by TOPMETR:7;
A2: for x being Point of S2 holds g.x = P.(1 - x`2)
proof
let x be Point of S2;
x in the carrier of S2;
then
A3: x in IBB by PRE_TOPC:8;
then
A4: x in the carrier of S;
then
A5: x in [:the carrier of I[01], the carrier of I[01]:] by BORSUK_1:def 2;
then
A6: x = [x`1,x`2] by MCART_1:21;
then
A7: x`2 in the carrier of I[01] by A5,ZFMISC_1:87;
x`1 in the carrier of I[01] by A5,A6,ZFMISC_1:87;
then
A8: e2.(x`1,x`2) = x`2 by A7,FUNCT_3:def 5;
A9: x in dom e2 by A4,FUNCT_2:def 1;
g.x = gg.x by A3,FUNCT_1:49
.= (-P).(e2.x) by A9,FUNCT_1:13
.= P.(1 - x`2) by A1,A6,A7,A8,BORSUK_2:def 6;
hence thesis;
end;
set S3 = S|ICC;
set S1 = S|IAA;
reconsider e1 = pr1(the carrier of I[01], the carrier of I[01]) as
continuous Function of S, I[01] by YELLOW12:39;
A10: a, a are_connected;
then reconsider PP = P + -P as continuous Path of a,a by BORSUK_2:def 2;
set ff = PP * e1;
reconsider f = ff|IAA as Function of S1, T by PRE_TOPC:9;
reconsider f as continuous Function of S1, T by TOPMETR:7;
set S12 = S | (IAA \/ IBB);
reconsider S12 as non empty SubSpace of S;
A11: the carrier of S12 = IAA \/ IBB by PRE_TOPC:8;
set hh = PP * e1;
reconsider h = hh|ICC as Function of S3, T by PRE_TOPC:9;
reconsider h as continuous Function of S3, T by TOPMETR:7;
A12: for x being Point of S3 holds h.x = (-P).(2 * x`1 - 1)
proof
let x be Point of S3;
x in the carrier of S3;
then
A13: x in ICC by PRE_TOPC:8;
then
A14: x`1 >= 1/2 by Th60;
A15: x in the carrier of S by A13;
then
A16: x in [:the carrier of I[01], the carrier of I[01]:] by BORSUK_1:def 2;
then
A17: x = [x`1,x`2] by MCART_1:21;
then
A18: x`1 in the carrier of I[01] by A16,ZFMISC_1:87;
x`2 in the carrier of I[01] by A16,A17,ZFMISC_1:87;
then
A19: e1.(x`1,x`2) = x`1 by A18,FUNCT_3:def 4;
A20: x in dom e1 by A15,FUNCT_2:def 1;
h.x = hh.x by A13,FUNCT_1:49
.= (P + - P).(e1.x) by A20,FUNCT_1:13
.= (-P).(2 * x`1 - 1) by A1,A17,A18,A19,A14,BORSUK_2:def 5;
hence thesis;
end;
A21: for x being Point of S1 holds f.x = P.(2 * x`1)
proof
let x be Point of S1;
x in the carrier of S1;
then
A22: x in IAA by PRE_TOPC:8;
then
A23: x`1 <= 1/2 by Th59;
A24: x in the carrier of S by A22;
then
A25: x in [:the carrier of I[01], the carrier of I[01]:] by BORSUK_1:def 2;
then
A26: x = [x`1,x`2] by MCART_1:21;
then
A27: x`1 in the carrier of I[01] by A25,ZFMISC_1:87;
x`2 in the carrier of I[01] by A25,A26,ZFMISC_1:87;
then
A28: e1.(x`1,x`2) = x`1 by A27,FUNCT_3:def 4;
A29: x in dom e1 by A24,FUNCT_2:def 1;
f.x = ff.x by A22,FUNCT_1:49
.= (P + -P).(e1.x) by A29,FUNCT_1:13
.= P.(2 * x`1) by A1,A26,A27,A28,A23,BORSUK_2:def 5;
hence thesis;
end;
A30: for p be object st p in ([#] S1) /\ ([#] S2) holds f.p = g.p
proof
let p be object;
assume p in ([#] S1) /\ ([#] S2);
then
A31: p in ([#] S1) /\ IBB by PRE_TOPC:def 5;
then
A32: p in IAA /\ IBB by PRE_TOPC:def 5;
then consider r being Point of S such that
A33: r = p and
A34: r`2 = 1 - 2 * (r`1) by Th57;
A35: 2 * r`1 = 1 - r`2 by A34;
p in IAA by A32,XBOOLE_0:def 4;
then reconsider pp = p as Point of S1 by PRE_TOPC:8;
p in IBB by A31,XBOOLE_0:def 4;
then
A36: pp is Point of S2 by PRE_TOPC:8;
f.p = P.(2 * pp`1) by A21
.= g.p by A2,A33,A35,A36;
hence thesis;
end;
reconsider s3 = [#]S3 as Subset of S by PRE_TOPC:def 5;
A37: s3 = ICC by PRE_TOPC:def 5;
A38: S1 is SubSpace of S12 & S2 is SubSpace of S12 by TOPMETR:22,XBOOLE_1:7;
A39: [#]S2 = IBB by PRE_TOPC:def 5;
A40: [#]S1 = IAA by PRE_TOPC:def 5;
then reconsider s1 = [#]S1, s2 = [#]S2 as Subset of S12 by A11,A39,XBOOLE_1:7
;
A41: s1 is closed by A40,TOPS_2:26;
A42: s2 is closed by A39,TOPS_2:26;
([#] S1) \/ ([#] S2) = [#] S12 by A11,A39,PRE_TOPC:def 5;
then consider fg being Function of S12, T such that
A43: fg = f +* g and
A44: fg is continuous by A30,A38,A41,A42,JGRAPH_2:1;
A45: [#]S3 = ICC by PRE_TOPC:def 5;
A46: for p be object st p in ([#] S12) /\ ([#] S3) holds fg.p = h.p
proof
let p be object;
[1/2,0] in IBB /\ ICC by Th66,Th67,XBOOLE_0:def 4;
then
A47: { [1/2,0] } c= IBB /\ ICC by ZFMISC_1:31;
assume p in ([#] S12) /\ ([#] S3);
then p in { [1/2,0] } \/ (IBB /\ ICC) by A11,A45,Th72,XBOOLE_1:23;
then
A48: p in IBB /\ ICC by A47,XBOOLE_1:12;
then p in ICC by XBOOLE_0:def 4;
then reconsider pp = p as Point of S3 by PRE_TOPC:8;
A49: p in IBB by A48,XBOOLE_0:def 4;
then
A50: pp is Point of S2 by PRE_TOPC:8;
A51: ex q being Point of S st q = p & q`2 = 2 * (q`1) - 1 by A48,Th58;
then
A52: 2 * pp`1 - 1 is Point of I[01] by Th27;
p in the carrier of S2 by A49,PRE_TOPC:8;
then p in dom g by FUNCT_2:def 1;
then fg.p = g.p by A43,FUNCT_4:13
.= P.(1 - pp`2) by A2,A50
.= (-P).(2 * pp`1 - 1) by A1,A51,A52,BORSUK_2:def 6
.= h.p by A12;
hence thesis;
end;
([#] S12) \/ ([#] S3) = (IAA \/ IBB) \/ ICC by A11,PRE_TOPC:def 5
.= [#] S by Th56,BORSUK_1:40,def 2;
then consider H being Function of S, T such that
A53: H = fg +* h and
A54: H is continuous by A11,A44,A46,A37,JGRAPH_2:1;
A55: for s being Point of I[01] holds H.(s,0) = (P+ -P).s & H.(s,1) = Q.s
proof
let s be Point of I[01];
thus H.(s,0) = (P+ -P).s
proof
A56: [s,0]`1 = s;
per cases by XXREAL_0:1;
suppose
A57: s < 1/2;
then not [s,0] in IBB by Th71;
then not [s,0] in the carrier of S2 by PRE_TOPC:8;
then
A58: not [s,0] in dom g;
[s,0] in IAA by A57,Th70;
then
A59: [s,0] in the carrier of S1 by PRE_TOPC:8;
not [s,0] in ICC by A57,Th71;
then not [s,0] in the carrier of S3 by PRE_TOPC:8;
then not [s,0] in dom h;
then H. [s,0] = fg. [s,0] by A53,FUNCT_4:11
.= f. [s,0] by A43,A58,FUNCT_4:11
.= P.(2 * s) by A21,A56,A59
.= (P+ -P).s by A1,A57,BORSUK_2:def 5;
hence thesis;
end;
suppose
A60: s = 1/2;
then
A61: [s,0] in the carrier of S3 by Th66,PRE_TOPC:8;
then [s,0] in dom h by FUNCT_2:def 1;
then H. [s,0] = h. [s,0] by A53,FUNCT_4:13
.= (-P).(2 * s - 1) by A12,A56,A61
.= b by A1,A60,BORSUK_2:def 2
.= P.(2 * (1/2)) by A1,BORSUK_2:def 2
.= (P+ -P).s by A1,A60,BORSUK_2:def 5;
hence thesis;
end;
suppose
A62: s > 1/2;
then [s,0] in ICC by Th69;
then
A63: [s,0] in the carrier of S3 by PRE_TOPC:8;
then [s,0] in dom h by FUNCT_2:def 1;
then H. [s,0] = h. [s,0] by A53,FUNCT_4:13
.= (-P).(2 * s - 1) by A12,A56,A63
.= (P+ -P).s by A1,A62,BORSUK_2:def 5;
hence thesis;
end;
end;
thus H.(s,1) = Q.s
proof
A64: [s,1]`2 = 1;
A65: [s,1]`1 = s;
A66: dom Q = the carrier of I[01] by FUNCT_2:def 1;
then
A67: 0 in dom Q by BORSUK_1:43;
per cases;
suppose
A68: s <> 1;
[s,1] in IBB by Th65;
then
A69: [s,1] in the carrier of S2 by PRE_TOPC:8;
then
A70: [s,1] in dom g by FUNCT_2:def 1;
not [s,1] in ICC by A68,Th63;
then not [s,1] in the carrier of S3 by PRE_TOPC:8;
then not [s,1] in dom h;
then H. [s,1] = fg. [s,1] by A53,FUNCT_4:11
.= g. [s,1] by A43,A70,FUNCT_4:13
.= P.(1 - 1) by A2,A64,A69
.= a by A1,BORSUK_2:def 2
.= Q.0 by A10,BORSUK_2:def 2
.= Q.s by A66,A67,FUNCT_1:def 10;
hence thesis;
end;
suppose
A71: s = 1;
then
A72: [s,1] in the carrier of S3 by Th66,PRE_TOPC:8;
then [s,1] in dom h by FUNCT_2:def 1;
then H. [s,1] = h. [s,1] by A53,FUNCT_4:13
.= (-P).(2 * s - 1) by A12,A65,A72
.= a by A1,A71,BORSUK_2:def 2
.= Q.0 by A10,BORSUK_2:def 2
.= Q.s by A66,A67,FUNCT_1:def 10;
hence thesis;
end;
end;
end;
for t being Point of I[01] holds H.(0,t) = a & H.(1,t) = a
proof
let t be Point of I[01];
thus H.(0,t) = a
proof
0 in the carrier of I[01] by BORSUK_1:43;
then reconsider x = [0,t] as Point of S by Lm1;
x in IAA by Th61;
then
A73: x is Point of S1 by PRE_TOPC:8;
x`1 = 0;
then not x in ICC by Th60;
then not x in the carrier of S3 by PRE_TOPC:8;
then
A74: not [0,t] in dom h;
per cases;
suppose
t <> 1;
then not x in IBB by Th62;
then not x in the carrier of S2 by PRE_TOPC:8;
then not x in dom g;
then fg. [0,t] = f. [0,t] by A43,FUNCT_4:11
.= P.(2 * x`1) by A21,A73
.= a by A1,BORSUK_2:def 2;
hence thesis by A53,A74,FUNCT_4:11;
end;
suppose
A75: t = 1;
then
A76: x in the carrier of S2 by Th64,PRE_TOPC:8;
then x in dom g by FUNCT_2:def 1;
then fg. [0,t] = g. [0,1] by A43,A75,FUNCT_4:13
.= P.(1 - x`2) by A2,A75,A76
.= a by A1,A75,BORSUK_2:def 2;
hence thesis by A53,A74,FUNCT_4:11;
end;
end;
thus H.(1,t) = a
proof
1 in the carrier of I[01] by BORSUK_1:43;
then reconsider x = [1,t] as Point of S by Lm1;
x in ICC by Th68;
then
A77: x in the carrier of S3 by PRE_TOPC:8;
then
A78: [1,t] in dom h by FUNCT_2:def 1;
h. [1,t] = (-P).(2 * x`1 - 1) by A12,A77
.= a by A1,BORSUK_2:def 2;
hence thesis by A53,A78,FUNCT_4:13;
end;
end;
hence thesis by A54,A55;
end;
theorem
for P being Path of a1, b1, Q being constant Path of a1, a1 holds P +
- P, Q are_homotopic by Th84,BORSUK_2:def 3;
theorem Th86:
for P being Path of b, a, Q being constant Path of a, a st b, a
are_connected holds - P + P, Q are_homotopic
proof
set S = [:I[01],I[01]:];
let P be Path of b, a, Q be constant Path of a, a such that
A1: b, a are_connected;
reconsider e2 = pr2(the carrier of I[01], the carrier of I[01]) as
continuous Function of S, I[01] by YELLOW12:40;
set gg = P * e2;
P is continuous by A1,BORSUK_2:def 2;
then reconsider gg as continuous Function of S, T;
set S2 = S|IBB;
reconsider g = gg|IBB as Function of S2, T by PRE_TOPC:9;
reconsider g as continuous Function of S2, T by TOPMETR:7;
A2: for x being Point of S2 holds g.x = (-P).(1 - x`2)
proof
let x be Point of S2;
x in the carrier of S2;
then
A3: x in IBB by PRE_TOPC:8;
then
A4: x in the carrier of S;
then
A5: x in [:the carrier of I[01], the carrier of I[01]:] by BORSUK_1:def 2;
then
A6: x = [x`1,x`2] by MCART_1:21;
then
A7: x`2 in the carrier of I[01] by A5,ZFMISC_1:87;
then
A8: 1 - x`2 in the carrier of I[01] by JORDAN5B:4;
x`1 in the carrier of I[01] by A5,A6,ZFMISC_1:87;
then
A9: e2.(x`1,x`2) = x`2 by A7,FUNCT_3:def 5;
A10: x in dom e2 by A4,FUNCT_2:def 1;
g.x = gg.(x`1,x`2) by A3,A6,FUNCT_1:49
.= P.(1 - (1 - x`2)) by A6,A9,A10,FUNCT_1:13
.= (-P).(1 - x`2) by A1,A8,BORSUK_2:def 6;
hence thesis;
end;
set S3 = S|ICC;
set S1 = S|IAA;
reconsider e1 = pr1(the carrier of I[01], the carrier of I[01]) as
continuous Function of S, I[01] by YELLOW12:39;
A11: a, a are_connected;
then reconsider PP = -P + P as continuous Path of a,a by BORSUK_2:def 2;
set ff = PP * e1;
reconsider f = ff|IAA as Function of S1, T by PRE_TOPC:9;
reconsider f as continuous Function of S1, T by TOPMETR:7;
set S12 = S | (IAA \/ IBB);
reconsider S12 as non empty SubSpace of S;
A12: the carrier of S12 = IAA \/ IBB by PRE_TOPC:8;
set hh = PP * e1;
reconsider h = hh|ICC as Function of S3, T by PRE_TOPC:9;
reconsider h as continuous Function of S3, T by TOPMETR:7;
A13: for x being Point of S3 holds h.x = P.(2 * x`1 - 1)
proof
let x be Point of S3;
x in the carrier of S3;
then
A14: x in ICC by PRE_TOPC:8;
then
A15: x`1 >= 1/2 by Th60;
A16: x in the carrier of S by A14;
then
A17: x in [:the carrier of I[01], the carrier of I[01]:] by BORSUK_1:def 2;
then
A18: x = [x`1,x`2] by MCART_1:21;
then
A19: x`1 in the carrier of I[01] by A17,ZFMISC_1:87;
x`2 in the carrier of I[01] by A17,A18,ZFMISC_1:87;
then
A20: e1.(x`1,x`2) = x`1 by A19,FUNCT_3:def 4;
A21: x in dom e1 by A16,FUNCT_2:def 1;
h.x = hh.x by A14,FUNCT_1:49
.= (-P + P).(e1.(x`1,x`2)) by A18,A21,FUNCT_1:13
.= P.(2 * x`1 - 1) by A1,A19,A20,A15,BORSUK_2:def 5;
hence thesis;
end;
A22: for x being Point of S1 holds f.x = (-P).(2 * x`1)
proof
let x be Point of S1;
x in the carrier of S1;
then
A23: x in IAA by PRE_TOPC:8;
then
A24: x`1 <= 1/2 by Th59;
A25: x in the carrier of S by A23;
then
A26: x in [:the carrier of I[01], the carrier of I[01]:] by BORSUK_1:def 2;
then
A27: x = [x`1,x`2] by MCART_1:21;
then
A28: x`1 in the carrier of I[01] by A26,ZFMISC_1:87;
x`2 in the carrier of I[01] by A26,A27,ZFMISC_1:87;
then
A29: e1.(x`1,x`2) = x`1 by A28,FUNCT_3:def 4;
A30: x in dom e1 by A25,FUNCT_2:def 1;
f.x = ff.x by A23,FUNCT_1:49
.= (-P + P).(e1.x) by A30,FUNCT_1:13
.= (-P).(2 * x`1) by A1,A27,A28,A29,A24,BORSUK_2:def 5;
hence thesis;
end;
A31: for p be object st p in ([#] S1) /\ ([#] S2) holds f.p = g.p
proof
let p be object;
assume p in ([#] S1) /\ ([#] S2);
then
A32: p in ([#] S1) /\ IBB by PRE_TOPC:def 5;
then
A33: p in IAA /\ IBB by PRE_TOPC:def 5;
then consider r being Point of S such that
A34: r = p and
A35: r`2 = 1 - 2 * (r`1) by Th57;
A36: 2 * r`1 = 1 - r`2 by A35;
p in IAA by A33,XBOOLE_0:def 4;
then reconsider pp = p as Point of S1 by PRE_TOPC:8;
p in IBB by A32,XBOOLE_0:def 4;
then
A37: pp is Point of S2 by PRE_TOPC:8;
f.p = (-P).(2 * pp`1) by A22
.= g.p by A2,A34,A36,A37;
hence thesis;
end;
reconsider s3 = [#]S3 as Subset of S by PRE_TOPC:def 5;
A38: s3 = ICC by PRE_TOPC:def 5;
A39: S1 is SubSpace of S12 & S2 is SubSpace of S12 by TOPMETR:22,XBOOLE_1:7;
A40: [#]S2 = IBB by PRE_TOPC:def 5;
A41: [#]S1 = IAA by PRE_TOPC:def 5;
then reconsider s1 = [#]S1, s2 = [#]S2 as Subset of S12 by A12,A40,XBOOLE_1:7
;
A42: s1 is closed by A41,TOPS_2:26;
A43: s2 is closed by A40,TOPS_2:26;
([#] S1) \/ ([#] S2) = [#] S12 by A12,A40,PRE_TOPC:def 5;
then consider fg being Function of S12, T such that
A44: fg = f +* g and
A45: fg is continuous by A31,A39,A42,A43,JGRAPH_2:1;
A46: [#]S3 = ICC by PRE_TOPC:def 5;
A47: for p be object st p in ([#] S12) /\ ([#] S3) holds fg.p = h.p
proof
let p be object;
[1/2,0] in IBB /\ ICC by Th66,Th67,XBOOLE_0:def 4;
then
A48: { [1/2,0] } c= IBB /\ ICC by ZFMISC_1:31;
assume p in ([#] S12) /\ ([#] S3);
then p in { [1/2,0] } \/ (IBB /\ ICC) by A12,A46,Th72,XBOOLE_1:23;
then
A49: p in IBB /\ ICC by A48,XBOOLE_1:12;
then p in ICC by XBOOLE_0:def 4;
then reconsider pp = p as Point of S3 by PRE_TOPC:8;
A50: ex q being Point of S st q = p & q`2 = 2 * (q`1) - 1 by A49,Th58;
pp`2 is Point of I[01] by A49,Th27;
then
A51: 1 - pp`2 in the carrier of I[01] by JORDAN5B:4;
A52: p in IBB by A49,XBOOLE_0:def 4;
then
A53: pp is Point of S2 by PRE_TOPC:8;
p in the carrier of S2 by A52,PRE_TOPC:8;
then p in dom g by FUNCT_2:def 1;
then fg.p = g.p by A44,FUNCT_4:13
.= (-P).(1 - pp`2) by A2,A53
.= P.(1 - (1 - pp`2)) by A1,A51,BORSUK_2:def 6
.= h.p by A13,A50;
hence thesis;
end;
([#] S12) \/ ([#] S3) = [#] S by A12,A46,Th56,BORSUK_1:40,def 2;
then consider H being Function of S, T such that
A54: H = fg +* h and
A55: H is continuous by A12,A45,A47,A38,JGRAPH_2:1;
A56: for s being Point of I[01] holds H.(s,0) = (-P + P).s & H.(s,1) = Q.s
proof
let s be Point of I[01];
thus H.(s,0) = (-P + P).s
proof
A57: [s,0]`1 = s;
per cases by XXREAL_0:1;
suppose
A58: s < 1/2;
then not [s,0] in IBB by Th71;
then not [s,0] in the carrier of S2 by PRE_TOPC:8;
then
A59: not [s,0] in dom g;
[s,0] in IAA by A58,Th70;
then
A60: [s,0] in the carrier of S1 by PRE_TOPC:8;
not [s,0] in ICC by A58,Th71;
then not [s,0] in the carrier of S3 by PRE_TOPC:8;
then not [s,0] in dom h;
then H. [s,0] = fg. [s,0] by A54,FUNCT_4:11
.= f. [s,0] by A44,A59,FUNCT_4:11
.= (-P).(2 * s) by A22,A57,A60
.= (-P + P).s by A1,A58,BORSUK_2:def 5;
hence thesis;
end;
suppose
A61: s = 1/2;
then
A62: [s,0] in the carrier of S3 by Th66,PRE_TOPC:8;
then [s,0] in dom h by FUNCT_2:def 1;
then H. [s,0] = h. [s,0] by A54,FUNCT_4:13
.= P.(2 * s - 1) by A13,A57,A62
.= b by A1,A61,BORSUK_2:def 2
.= (-P).(2 * (1/2)) by A1,BORSUK_2:def 2
.= (-P + P).s by A1,A61,BORSUK_2:def 5;
hence thesis;
end;
suppose
A63: s > 1/2;
then [s,0] in ICC by Th69;
then
A64: [s,0] in the carrier of S3 by PRE_TOPC:8;
then [s,0] in dom h by FUNCT_2:def 1;
then H. [s,0] = h. [s,0] by A54,FUNCT_4:13
.= P.(2 * s - 1) by A13,A57,A64
.= (-P + P).s by A1,A63,BORSUK_2:def 5;
hence thesis;
end;
end;
thus H.(s,1) = Q.s
proof
A65: [s,1]`2 = 1;
A66: [s,1]`1 = s;
A67: dom Q = the carrier of I[01] by FUNCT_2:def 1;
then
A68: 0 in dom Q by BORSUK_1:43;
per cases;
suppose
A69: s <> 1;
[s,1] in IBB by Th65;
then
A70: [s,1] in the carrier of S2 by PRE_TOPC:8;
then
A71: [s,1] in dom g by FUNCT_2:def 1;
not [s,1] in ICC by A69,Th63;
then not [s,1] in the carrier of S3 by PRE_TOPC:8;
then not [s,1] in dom h;
then H. [s,1] = fg. [s,1] by A54,FUNCT_4:11
.= g. [s,1] by A44,A71,FUNCT_4:13
.= (-P).(1 - 1) by A2,A65,A70
.= a by A1,BORSUK_2:def 2
.= Q.0 by A11,BORSUK_2:def 2
.= Q.s by A67,A68,FUNCT_1:def 10;
hence thesis;
end;
suppose
A72: s = 1;
then
A73: [s,1] in the carrier of S3 by Th66,PRE_TOPC:8;
then [s,1] in dom h by FUNCT_2:def 1;
then H. [s,1] = h. [s,1] by A54,FUNCT_4:13
.= P.(2 * s - 1) by A13,A66,A73
.= a by A1,A72,BORSUK_2:def 2
.= Q.0 by A11,BORSUK_2:def 2
.= Q.s by A67,A68,FUNCT_1:def 10;
hence thesis;
end;
end;
end;
for t being Point of I[01] holds H.(0,t) = a & H.(1,t) = a
proof
let t be Point of I[01];
thus H.(0,t) = a
proof
0 in the carrier of I[01] by BORSUK_1:43;
then reconsider x = [0,t] as Point of S by Lm1;
x in IAA by Th61;
then
A74: x is Point of S1 by PRE_TOPC:8;
x`1 = 0;
then not x in ICC by Th60;
then not x in the carrier of S3 by PRE_TOPC:8;
then
A75: not [0,t] in dom h;
per cases;
suppose
t <> 1;
then not x in IBB by Th62;
then not x in the carrier of S2 by PRE_TOPC:8;
then not x in dom g;
then fg. [0,t] = f. [0,t] by A44,FUNCT_4:11
.= (-P).(2 * x`1) by A22,A74
.= a by A1,BORSUK_2:def 2;
hence thesis by A54,A75,FUNCT_4:11;
end;
suppose
A76: t = 1;
then
A77: x in the carrier of S2 by Th64,PRE_TOPC:8;
then x in dom g by FUNCT_2:def 1;
then fg. [0,t] = g. [0,1] by A44,A76,FUNCT_4:13
.= (-P).(1 - x`2) by A2,A76,A77
.= a by A1,A76,BORSUK_2:def 2;
hence thesis by A54,A75,FUNCT_4:11;
end;
end;
thus H.(1,t) = a
proof
1 in the carrier of I[01] by BORSUK_1:43;
then reconsider x = [1,t] as Point of S by Lm1;
x in ICC by Th68;
then
A78: x in the carrier of S3 by PRE_TOPC:8;
then
A79: [1,t] in dom h by FUNCT_2:def 1;
h. [1,t] = P.(2 * x`1 - 1) by A13,A78
.= a by A1,BORSUK_2:def 2;
hence thesis by A54,A79,FUNCT_4:13;
end;
end;
hence thesis by A55,A56;
end;
theorem
for P being Path of b1, a1, Q being constant Path of a1, a1 holds - P
+ P, Q are_homotopic by Th86,BORSUK_2:def 3;
theorem
for P, Q be constant Path of a, a holds P, Q are_homotopic
proof
let P, Q be constant Path of a, a;
P = I[01] --> a & Q = I[01] --> a by BORSUK_2:5;
hence thesis by BORSUK_2:12;
end;
definition
let T be non empty TopSpace;
let a, b be Point of T;
let P, Q be Path of a, b;
assume
A1: P, Q are_homotopic;
mode Homotopy of P, Q -> Function of [:I[01],I[01]:], T means
it is
continuous & for t being Point of I[01] holds it.(t,0) = P.t & it.(t,1) = Q.t &
it.(0,t) = a & it.(1,t) = b;
existence by A1;
end;