:: Introduction to Homotopy Theory
:: by Adam Grabowski
::
:: Received September 10, 1997
:: Copyright (c) 1997-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, PRE_TOPC, CARD_1, XXREAL_0, STRUCT_0,
BORSUK_1, XXREAL_1, REAL_1, SUBSET_1, TARSKI, FUNCT_1, RELAT_1, RCOMP_1,
ORDINAL2, FUNCT_4, TOPS_2, FUNCOP_1, GRAPH_1, RELAT_2, ARYTM_3, ARYTM_1,
TOPMETR, TREAL_1, VALUED_1, SETFAM_1, ZFMISC_1, PCOMPS_1, MCART_1,
CONNSP_2, TOPS_1, BORSUK_2;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, ORDINAL1, CARD_1,
NUMBERS, XXREAL_0, XCMPLX_0, XREAL_0, REAL_1, RELAT_1, FUNCT_1, RELSET_1,
PARTFUN1, FUNCT_2, DOMAIN_1, STRUCT_0, PRE_TOPC, TOPS_2, XTUPLE_0,
MCART_1, RCOMP_1, PCOMPS_1, TOPS_1, COMPTS_1, CONNSP_1, CONNSP_2,
TREAL_1, FUNCT_4, BORSUK_1, T_0TOPSP, TOPMETR, BINOP_1, FUNCT_3;
constructors SETFAM_1, FUNCT_3, FUNCT_4, REAL_1, MEMBERED, RCOMP_1, TOPS_1,
CONNSP_1, TOPS_2, COMPTS_1, URYSOHN1, T_0TOPSP, TREAL_1, FUNCOP_1,
PCOMPS_1, XXREAL_2, COMPLEX1, XTUPLE_0, BINOP_1;
registrations XBOOLE_0, SUBSET_1, FUNCT_1, FUNCT_2, XREAL_0, MEMBERED,
STRUCT_0, PRE_TOPC, COMPTS_1, METRIC_1, BORSUK_1, RELAT_1, XXREAL_2,
TOPS_1, CONNSP_1, TOPMETR, RELSET_1, XTUPLE_0;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI, PRE_TOPC, URYSOHN1, T_0TOPSP, XBOOLE_0;
equalities TARSKI, BINOP_1, STRUCT_0, BORSUK_1;
expansions PRE_TOPC, T_0TOPSP, BORSUK_1;
theorems BORSUK_1, FUNCOP_1, TOPS_2, TREAL_1, FUNCT_2, FUNCT_1, PRE_TOPC,
RCOMP_1, TARSKI, RELAT_1, TOPS_1, URYSOHN1, TOPMETR, FUNCT_4, HEINE,
PCOMPS_1, MCART_1, ZFMISC_1, CONNSP_2, FUNCT_3, COMPTS_1, T_0TOPSP,
CARD_1, RELSET_1, XBOOLE_0, XBOOLE_1, XREAL_1, XXREAL_1, XXREAL_2;
schemes FUNCT_2, FUNCT_1;
begin :: Preliminaries
reserve T,T1,T2,S for non empty TopSpace;
Lm1: for r being Real holds 0 <= r & r <= 1 iff r in the carrier of
I[01]
proof
let r be Real;
A1: [.0,1.] = { r1 where r1 is Real: 0 <= r1 & r1 <= 1 }
by RCOMP_1:def 1;
thus 0 <= r & r <= 1 implies r in the carrier of I[01] by A1,BORSUK_1:40;
assume r in the carrier of I[01];
then ex r2 being Real st r2 = r & 0 <= r2 & r2 <= 1 by A1,BORSUK_1:40;
hence thesis;
end;
scheme
FrCard { A() -> non empty set, X() -> set, F(object) -> set, P[set] }:
card { F
(w) where w is Element of A(): w in X() & P[w] } c= card X() proof
consider f be Function such that
A1: dom f = X() &
for x be object st x in X() holds f.x = F(x) from FUNCT_1
:sch 3;
{ F(w) where w is Element of A(): w in X() & P[w]} c= rng f
proof
let x be object;
assume x in { F(w) where w is Element of A(): w in X() & P[w]};
then consider w being Element of A() such that
A2: x = F(w) and
A3: w in X() and
P[w];
f.w = x by A1,A2,A3;
hence thesis by A1,A3,FUNCT_1:def 3;
end;
hence thesis by A1,CARD_1:12;
end;
theorem
for f being Function of T1,S, g being Function of T2,S st T1 is
SubSpace of T & T2 is SubSpace of T & ([#] T1) \/ ([#] T2) = [#] T & T1 is
compact & T2 is compact & T is T_2 & f is continuous & g is continuous & ( for
p be set st p in ([#] T1) /\ ([#] T2) holds f.p = g.p ) ex h being Function of
T,S st h = f+*g & h is continuous
proof
let f be Function of T1,S, g be Function of T2,S;
assume that
A1: T1 is SubSpace of T and
A2: T2 is SubSpace of T and
A3: ([#] T1) \/ ([#] T2) = [#] T and
A4: T1 is compact and
A5: T2 is compact and
A6: T is T_2 and
A7: f is continuous and
A8: g is continuous and
A9: for p be set st p in ([#] T1) /\ ([#] T2) holds f.p = g.p;
set h = f+*g;
A10: dom g = [#] T2 by FUNCT_2:def 1;
A11: dom f = [#] T1 by FUNCT_2:def 1;
then
A12: dom h = the carrier of T by A3,A10,FUNCT_4:def 1;
rng h c= rng f \/ rng g by FUNCT_4:17;
then reconsider h as Function of T,S by A12,FUNCT_2:2,XBOOLE_1:1;
take h;
thus h = f+*g;
for P being Subset of S st P is closed holds h"P is closed
proof
let P be Subset of S;
reconsider P3 = f"P as Subset of T1;
reconsider P4 = g"P as Subset of T2;
[#] T1 c= [#] T by A3,XBOOLE_1:7;
then reconsider P1 = f"P as Subset of T by XBOOLE_1:1;
[#] T2 c= [#] T by A3,XBOOLE_1:7;
then reconsider P2 = g"P as Subset of T by XBOOLE_1:1;
A13: dom h = dom f \/ dom g by FUNCT_4:def 1;
A14: now
let x be object;
thus x in h"P /\ [#] T2 implies x in g"P
proof
assume
A15: x in h"P /\ [#] T2;
then x in h"P by XBOOLE_0:def 4;
then
A16: h.x in P by FUNCT_1:def 7;
g.x = h.x by A10,A15,FUNCT_4:13;
hence thesis by A10,A15,A16,FUNCT_1:def 7;
end;
assume
A17: x in g"P;
then
A18: x in dom g by FUNCT_1:def 7;
g.x in P by A17,FUNCT_1:def 7;
then
A19: h.x in P by A18,FUNCT_4:13;
x in dom h by A13,A18,XBOOLE_0:def 3;
then x in h"P by A19,FUNCT_1:def 7;
hence x in h"P /\ [#] T2 by A17,XBOOLE_0:def 4;
end;
A20: for x being set st x in [#] T1 holds h.x = f.x
proof
let x be set such that
A21: x in [#] T1;
now
per cases;
suppose
A22: x in [#] T2;
then x in [#] T1 /\ [#] T2 by A21,XBOOLE_0:def 4;
then f.x = g.x by A9;
hence thesis by A10,A22,FUNCT_4:13;
end;
suppose
not x in [#] T2;
hence thesis by A10,FUNCT_4:11;
end;
end;
hence thesis;
end;
now
let x be object;
thus x in h"P /\ [#] T1 implies x in f"P
proof
assume
A23: x in h"P /\ [#] T1;
then x in h"P by XBOOLE_0:def 4;
then
A24: h.x in P by FUNCT_1:def 7;
f.x = h.x by A20,A23;
hence thesis by A11,A23,A24,FUNCT_1:def 7;
end;
assume
A25: x in f"P;
then x in dom f by FUNCT_1:def 7;
then
A26: x in dom h by A13,XBOOLE_0:def 3;
f.x in P by A25,FUNCT_1:def 7;
then h.x in P by A20,A25;
then x in h"P by A26,FUNCT_1:def 7;
hence x in h"P /\ [#] T1 by A25,XBOOLE_0:def 4;
end;
then
A27: h"P /\ [#] T1 = f"P by TARSKI:2;
assume
A28: P is closed;
then P3 is closed by A7;
then P3 is compact by A4,COMPTS_1:8;
then
A29: P1 is compact by A1,COMPTS_1:19;
P4 is closed by A8,A28;
then P4 is compact by A5,COMPTS_1:8;
then
A30: P2 is compact by A2,COMPTS_1:19;
h"P = h"P /\ ([#] T1 \/ [#] T2) by A11,A10,A13,RELAT_1:132,XBOOLE_1:28
.= (h"P /\ [#](T1)) \/ (h"P /\ [#](T2)) by XBOOLE_1:23;
then h"P = f"P \/ g"P by A27,A14,TARSKI:2;
hence thesis by A6,A29,A30;
end;
hence thesis;
end;
registration
let T be TopStruct;
cluster id T -> open continuous;
coherence
by FUNCT_1:92,FUNCT_2:94;
end;
registration
let T be TopStruct;
cluster continuous one-to-one for Function of T, T;
existence
proof
take id T;
thus thesis;
end;
end;
theorem
for S, T being non empty TopSpace, f being Function of S, T st f is
being_homeomorphism holds f" is open
proof
let S, T be non empty TopSpace, f be Function of S, T;
assume f is being_homeomorphism;
then
A1: rng f = [#] T & f is one-to-one continuous by TOPS_2:def 5;
let P be Subset of T;
f"P = (f").:P by A1,TOPS_2:55;
hence thesis by A1,TOPS_2:43;
end;
begin :: Paths and arcwise connected spaces
theorem Th3:
for T be non empty TopSpace, a be Point of T ex f be Function of
I[01], T st f is continuous & f.0 = a & f.1 = a
proof
let T be non empty TopSpace, a be Point of T;
take I[01] --> a;
thus thesis by BORSUK_1:def 14,def 15,FUNCOP_1:7;
end;
definition
let T be TopStruct, a,b be Point of T;
pred a,b are_connected means
ex f being Function of I[01], T st f is continuous & f.0 = a & f.1 = b;
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
by Th3;
end;
definition
let T be TopStruct;
let a, b be Point of T;
assume
A1: a, b are_connected;
mode Path of a, b -> Function of I[01], T means
:Def2:
it is continuous & it .0 = a & it.1 = b;
existence by A1;
end;
registration
let T be non empty TopSpace;
let a be Point of T;
cluster continuous for Path of a, a;
existence
proof
set IT = I[01] --> a;
A1: a,a are_connected;
IT.0 = a & IT.1 = a by BORSUK_1:def 14,def 15,FUNCOP_1:7;
then IT is Path of a, a by A1,Def2;
hence thesis;
end;
end;
definition
let T be TopStruct;
attr T is pathwise_connected means
:Def3:
for a, b being Point of T holds a, b are_connected;
correctness;
end;
registration
cluster strict pathwise_connected non empty for TopSpace;
existence
proof
set T = I[01] | { 0[01] };
0[01] in { 0[01] } by TARSKI:def 1;
then reconsider nl = 0[01] as Point of T by PRE_TOPC:8;
A1: the carrier of T = { 0[01] } by PRE_TOPC:8;
for a, b being Point of T holds a,b are_connected
proof
reconsider f = I[01] --> nl as Function of I[01], T;
let a, b be Point of T;
take f;
thus f is continuous;
a = nl & b = nl by A1,TARSKI:def 1;
hence thesis by BORSUK_1:def 15,FUNCOP_1:7;
end;
then T is pathwise_connected;
hence thesis;
end;
end;
definition
let T be pathwise_connected TopStruct;
let a, b be Point of T;
redefine mode Path of a, b means :: redefines Path (BORSUK_2, definition)
:Def4:
it is continuous & it.0 = a & it.1 = b;
compatibility
proof
a,b are_connected by Def3;
hence thesis by Def2;
end;
end;
registration
let T be pathwise_connected TopStruct;
let a, b be Point of T;
cluster -> continuous for Path of a, b;
coherence by Def4;
end;
reserve GY for non empty TopSpace,
r,s for Real;
Lm2: 0 in [.0,1.] & 1 in [.0,1.] by XXREAL_1:1;
registration
cluster pathwise_connected -> connected for non empty TopSpace;
coherence
proof
let GX be non empty TopSpace;
assume
A1: for x,y being Point of GX holds x,y are_connected;
for x, y being Point of GX ex GY st (GY is connected & ex f being
Function of GY,GX st f is continuous & x in rng f & y in rng f)
proof
let x, y be Point of GX;
x,y are_connected by A1;
then consider h being Function of I[01],GX such that
A2: h is continuous and
A3: x=h.0 and
A4: y=h.1;
1 in dom h by Lm2,BORSUK_1:40,FUNCT_2:def 1;
then
A5: y in rng h by A4,FUNCT_1:def 3;
0 in dom h by Lm2,BORSUK_1:40,FUNCT_2:def 1;
then x in rng h by A3,FUNCT_1:def 3;
hence thesis by A2,A5,TREAL_1:19;
end;
hence thesis by TOPS_2:63;
end;
end;
begin :: Basic operations on paths
Lm3: for G being non empty TopSpace, w1,w2,w3 being Point of G, h1,h2 being
Function of I[01],G st h1 is continuous & w1=h1.0 & w2=h1.1 & h2 is continuous
& w2=h2.0 & w3=h2.1 holds ex h3 being Function of I[01],G st h3 is continuous &
w1=h3.0 & w3=h3.1 & rng h3 c= (rng h1) \/ (rng h2)
proof
let G be non empty TopSpace, w1,w2,w3 be Point of G, h1,h2 be Function of
I[01],G;
assume that
A1: h1 is continuous and
A2: w1=h1.0 and
A3: w2=h1.1 and
A4: h2 is continuous and
A5: w2=h2.0 and
A6: w3=h2.1;
w2,w3 are_connected by A4,A5,A6;
then reconsider g2=h2 as Path of w2,w3 by A4,A5,A6,Def2;
w1,w2 are_connected by A1,A2,A3;
then reconsider g1=h1 as Path of w1,w2 by A1,A2,A3,Def2;
set P1=g1,P2=g2,p1=w1,p3=w3;
ex P0 being Path of p1,p3 st P0 is continuous & P0.0=p1 & P0.1=p3 & for
t being Point of I[01], t9 being Real st t = t9 holds ( 0 <= t9 & t9 <= 1/2
implies P0.t = P1.(2*t9) ) & ( 1/2 <= t9 & t9 <= 1 implies P0.t = P2.(2*t9-1) )
proof
1/2 in { r : 0 <= r & r <= 1 };
then reconsider pol = 1/2 as Point of I[01] by BORSUK_1:40,RCOMP_1:def 1;
reconsider T1 = Closed-Interval-TSpace (0, 1/2), T2 =
Closed-Interval-TSpace (1/2, 1) as SubSpace of I[01] by TOPMETR:20,TREAL_1:3;
set e2 = P[01](1/2, 1, (#)(0,1), (0,1)(#));
set e1 = P[01](0, 1/2, (#)(0,1), (0,1)(#));
set E1 = P1 * e1;
set E2 = P2 * e2;
set f = E1 +* E2;
A7: dom e1 = the carrier of Closed-Interval-TSpace(0,1/2) by FUNCT_2:def 1
.= [.0,1/2.] by TOPMETR:18;
A8: dom e2 = the carrier of Closed-Interval-TSpace(1/2,1) by FUNCT_2:def 1
.= [.1/2,1.] by TOPMETR:18;
reconsider gg = E2 as Function of T2, G by TOPMETR:20;
reconsider ff = E1 as Function of T1, G by TOPMETR:20;
A9: for t9 being Real st 1/2 <= t9 & t9 <= 1 holds E2.t9 = P2.(2*t9-1)
proof
reconsider r1 = (#)(0,1), r2 = (0,1)(#) as Real;
dom e2 = the carrier of Closed-Interval-TSpace(1/2,1) by FUNCT_2:def 1;
then
A10: dom e2 = [.1/2,1.] by TOPMETR:18
.= {r : 1/2 <= r & r <= 1 } by RCOMP_1:def 1;
let t9 be Real;
assume 1/2 <= t9 & t9 <= 1;
then
A11: t9 in dom e2 by A10;
then reconsider s = t9 as Point of Closed-Interval-TSpace (1/2,1);
e2.s = ((r2 - r1)/(1 - 1/2))*t9 + (1 * r1 - (1/2)*r2)/(1 - 1/2) by
TREAL_1:11
.= 2*t9 - 1 by TREAL_1:5;
hence thesis by A11,FUNCT_1:13;
end;
A12: for t9 being Real st 0 <= t9 & t9 <= 1/2 holds E1.t9 = P1.(2*t9)
proof
reconsider r1 = (#)(0,1), r2 = (0,1)(#) as Real;
dom e1 = the carrier of Closed-Interval-TSpace(0,1/2) by FUNCT_2:def 1;
then
A13: dom e1 = [.0, 1/2.] by TOPMETR:18
.= {r : 0 <= r & r <= 1/2 } by RCOMP_1:def 1;
let t9 be Real;
assume 0 <= t9 & t9 <= 1/2;
then
A14: t9 in dom e1 by A13;
then reconsider s = t9 as Point of Closed-Interval-TSpace (0, 1/2);
e1.s = ((r2 - r1)/(1/2 - 0))*t9 + ((1/2)*r1 - 0 * r2)/(1/2 - 0) by
TREAL_1:11
.= 2*t9 by TREAL_1:5;
hence thesis by A14,FUNCT_1:13;
end;
then
A15: ff.(1/2) = P2.(2*(1/2)-1) by A3,A5
.= gg.pol by A9;
[#] T1 = [.0,1/2.] & [#] T2 = [.1/2,1.] by TOPMETR:18;
then
A16: ([#] T1) \/ ([#] T2) = [#] I[01] & ([#] T1) /\ ([#] T2) = {pol} by
BORSUK_1:40,XXREAL_1:174,418;
A17: T2 is compact by HEINE:4;
dom P1 = the carrier of I[01] by FUNCT_2:def 1;
then
A18: rng e1 c= dom P1 by TOPMETR:20;
dom P2 = the carrier of I[01] & rng e2 c= the carrier of
Closed-Interval-TSpace(0,1) by FUNCT_2:def 1;
then
A19: dom E2 = dom e2 by RELAT_1:27,TOPMETR:20;
not 0 in { r : 1/2 <= r & r <= 1 }
proof
assume 0 in { r : 1/2 <= r & r <= 1 };
then ex rr being Real st rr = 0 & 1/2 <= rr & rr <= 1;
hence thesis;
end;
then not 0 in dom E2 by A8,A19,RCOMP_1:def 1;
then
A20: f.0 = E1.0 by FUNCT_4:11
.= P1.(2*0) by A12
.= p1 by A2;
A21: dom f = dom E1 \/ dom E2 by FUNCT_4:def 1
.= [.0,1/2.] \/ [.1/2,1.] by A7,A8,A18,A19,RELAT_1:27
.= the carrier of I[01] by BORSUK_1:40,XXREAL_1:174;
rng f c= rng E1 \/ rng E2 by FUNCT_4:17;
then
A22: rng f c= the carrier of G by XBOOLE_1:1;
A23: R^1 is T_2 & T1 is compact by HEINE:4,PCOMPS_1:34,TOPMETR:def 6;
reconsider f as Function of I[01], G by A21,A22,FUNCT_2:def 1,RELSET_1:4;
e1 is continuous & e2 is continuous by TREAL_1:12;
then reconsider f as continuous Function of I[01], G by A1,A4,A15,A16,A23
,A17,COMPTS_1:20,TOPMETR:20;
1 in { r : 1/2 <= r & r <= 1 };
then 1 in dom E2 by A8,A19,RCOMP_1:def 1;
then
A24: f.1 = E2.1 by FUNCT_4:13
.= P2.(2*1-1) by A9
.= p3 by A6;
then p1,p3 are_connected by A20;
then reconsider f as Path of p1, p3 by A20,A24,Def2;
for t being Point of I[01], t9 being Real st t = t9 holds ( 0 <= t9 &
t9 <= 1/2 implies f.t = P1.(2*t9) ) & ( 1/2 <= t9 & t9 <= 1 implies f.t = P2.(2
*t9-1) )
proof
let t be Point of I[01], t9 be Real;
assume
A25: t = t9;
thus 0 <= t9 & t9 <= 1/2 implies f.t = P1.(2*t9)
proof
assume
A26: 0 <= t9 & t9 <= 1/2;
then t9 in { r : 0 <= r & r <= 1/2 };
then
A27: t9 in [.0,1/2.] by RCOMP_1:def 1;
per cases;
suppose
A28: t9 <> 1/2;
not t9 in dom E2
proof
assume t9 in dom E2;
then t9 in [.0,1/2.] /\ [.1/2,1.] by A8,A19,A27,
XBOOLE_0:def 4;
then t9 in {1/2} by XXREAL_1:418;
hence thesis by A28,TARSKI:def 1;
end;
then f.t = E1.t by A25,FUNCT_4:11
.= P1.(2*t9) by A12,A25,A26;
hence thesis;
end;
suppose
A29: t9 = 1/2;
1/2 in { r : 1/2 <= r & r <= 1 };
then 1/2 in [.1/2, 1.] by RCOMP_1:def 1;
then 1/2 in the carrier of Closed-Interval-TSpace(1/2,1) by
TOPMETR:18;
then t in dom E2 by A25,A29,FUNCT_2:def 1,TOPMETR:20;
then f.t = E2.(1/2) by A25,A29,FUNCT_4:13
.= P1.(2*t9) by A12,A15,A29;
hence thesis;
end;
end;
thus 1/2 <= t9 & t9 <= 1 implies f.t = P2.(2*t9-1)
proof
assume
A30: 1/2 <= t9 & t9 <= 1;
then t9 in { r : 1/2 <= r & r <= 1 };
then t9 in [.1/2,1.] by RCOMP_1:def 1;
then f.t = E2.t by A8,A19,A25,FUNCT_4:13
.= P2.(2*t9-1) by A9,A25,A30;
hence thesis;
end;
end;
hence thesis by A20,A24;
end;
then consider P0 being Path of p1,p3 such that
A31: P0 is continuous & P0.0=p1 & P0.1=p3 and
A32: for t being Point of I[01], t9 being Real st t = t9 holds ( 0 <= t9
& t9 <= 1/2 implies P0.t = P1.(2*t9) ) & ( 1/2 <= t9 & t9 <= 1 implies P0.t =
P2.(2*t9-1) );
rng P0 c= (rng P1) \/ (rng P2)
proof
A33: dom g2=the carrier of I[01] by FUNCT_2:def 1;
let x be object;
A34: dom g1=the carrier of I[01] by FUNCT_2:def 1;
assume x in rng P0;
then consider z being object such that
A35: z in dom P0 and
A36: x=P0.z by FUNCT_1:def 3;
reconsider r=z as Real by A35;
A37: 0<=r by A35,BORSUK_1:40,XXREAL_1:1;
A38: r<=1 by A35,BORSUK_1:40,XXREAL_1:1;
per cases;
suppose
A39: r<=1/2;
then
A40: 2*r <= 2*(1/2) by XREAL_1:64;
0<=2*r by A37,XREAL_1:127;
then
A41: 2*r in the carrier of I[01] by A40,BORSUK_1:40,XXREAL_1:1;
P0.z=P1.(2*r) by A32,A35,A37,A39;
then P0.z in rng g1 by A34,A41,FUNCT_1:def 3;
hence thesis by A36,XBOOLE_0:def 3;
end;
suppose
A42: r>1/2;
2*r<=2*1 by A38,XREAL_1:64;
then 2*r<=1+1;
then
A43: 2*r-1<=1 by XREAL_1:20;
2*(1/2)=1;
then 0+1<=2*r by A42,XREAL_1:64;
then 0<=2*r-1 by XREAL_1:19;
then
A44: 2*r-1 in the carrier of I[01] by A43,BORSUK_1:40,XXREAL_1:1;
P0.z=P2.(2*r-1) by A32,A35,A38,A42;
then P0.z in rng g2 by A33,A44,FUNCT_1:def 3;
hence thesis by A36,XBOOLE_0:def 3;
end;
end;
hence thesis by A31;
end;
definition
let T be non empty TopSpace;
let a, b, c be Point of T;
let P be Path of a, b, Q be Path of b, c such that
A1: a,b are_connected and
A2: b,c are_connected;
func P + Q -> Path of a, c means
:Def5:
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) );
existence
proof
1/2 in { r : 0 <= r & r <= 1 };
then reconsider pol = 1/2 as Point of I[01] by BORSUK_1:40,RCOMP_1:def 1;
reconsider T1 = Closed-Interval-TSpace (0, 1/2), T2 =
Closed-Interval-TSpace (1/2, 1) as SubSpace of I[01] by TOPMETR:20,TREAL_1:3;
set e2 = P[01](1/2, 1, (#)(0,1), (0,1)(#));
set e1 = P[01](0, 1/2, (#)(0,1), (0,1)(#));
set E1 = P * e1;
set E2 = Q * e2;
set f = E1 +* E2;
A3: dom e1 = the carrier of Closed-Interval-TSpace(0,1/2) by FUNCT_2:def 1
.= [.0,1/2.] by TOPMETR:18;
A4: dom e2 = the carrier of Closed-Interval-TSpace(1/2,1) by FUNCT_2:def 1
.= [.1/2,1.] by TOPMETR:18;
A5: for t9 being Real st 1/2 <= t9 & t9 <= 1 holds E2.t9 = Q.(2*t9-1)
proof
reconsider r1 = (#)(0,1), r2 = (0,1)(#) as Real;
dom e2 = the carrier of Closed-Interval-TSpace(1/2,1) by FUNCT_2:def 1;
then
A6: dom e2 = [.1/2,1.] by TOPMETR:18
.= {r : 1/2 <= r & r <= 1 } by RCOMP_1:def 1;
let t9 be Real;
assume 1/2 <= t9 & t9 <= 1;
then
A7: t9 in dom e2 by A6;
then reconsider s = t9 as Point of Closed-Interval-TSpace (1/2,1);
e2.s = ((r2 - r1)/(1 - 1/2))*t9 + (1*r1 - (1/2)*r2)/(1 - 1/2) by
TREAL_1:11
.= 2*t9 - 1 by TREAL_1:5;
hence thesis by A7,FUNCT_1:13;
end;
reconsider gg = E2 as Function of T2, T by TOPMETR:20;
reconsider ff = E1 as Function of T1, T by TOPMETR:20;
A8: e1 is continuous Function of Closed-Interval-TSpace(0,1/2),
Closed-Interval-TSpace(0,1) & e2 is continuous by TREAL_1:12;
rng f c= rng E1 \/ rng E2 by FUNCT_4:17;
then
A9: rng f c= the carrier of T by XBOOLE_1:1;
A10: R^1 is T_2 & T1 is compact by HEINE:4,PCOMPS_1:34,TOPMETR:def 6;
A11: for t9 being Real st 0 <= t9 & t9 <= 1/2 holds E1.t9 = P.(2*t9)
proof
reconsider r1 = (#)(0,1), r2 = (0,1)(#) as Real;
dom e1 = the carrier of Closed-Interval-TSpace(0,1/2) by FUNCT_2:def 1;
then
A12: dom e1 = [.0, 1/2.] by TOPMETR:18
.= {r : 0 <= r & r <= 1/2 } by RCOMP_1:def 1;
let t9 be Real;
assume 0 <= t9 & t9 <= 1/2;
then
A13: t9 in dom e1 by A12;
then reconsider s = t9 as Point of Closed-Interval-TSpace (0, 1/2);
e1.s = ((r2 - r1)/(1/2 - 0))*t9 + ((1/2)*r1 - 0 * r2)/(1/2) by TREAL_1:11
.= 2*t9 by TREAL_1:5;
hence thesis by A13,FUNCT_1:13;
end;
then
A14: ff.(1/2) = P.(2*(1/2)) .= b by A1,Def2
.= Q.(2*(1/2)-1) by A2,Def2
.= gg.pol by A5;
dom P = the carrier of I[01] by FUNCT_2:def 1;
then
A15: rng e1 c= dom P by TOPMETR:20;
dom Q = the carrier of I[01] & rng e2 c= the carrier of
Closed-Interval-TSpace(0,1) by FUNCT_2:def 1;
then
A16: dom E2 = dom e2 by RELAT_1:27,TOPMETR:20;
not 0 in { r : 1/2 <= r & r <= 1 }
proof
assume 0 in { r : 1/2 <= r & r <= 1 };
then ex rr being Real st rr = 0 & 1/2 <= rr & rr <= 1;
hence thesis;
end;
then not 0 in dom E2 by A4,A16,RCOMP_1:def 1;
then
A17: f.0 = E1.0 by FUNCT_4:11
.= P.(2*0) by A11
.= a by A1,Def2;
A18: dom f = dom E1 \/ dom E2 by FUNCT_4:def 1
.= [.0,1/2.] \/ [.1/2,1.] by A3,A4,A15,A16,RELAT_1:27
.= the carrier of I[01] by BORSUK_1:40,XXREAL_1:174;
[#] T1 = [.0,1/2.] & [#] T2 = [.1/2,1.] by TOPMETR:18;
then
A19: ([#] T1) \/ ([#] T2) = [#] I[01] & ([#] T1) /\ ([#] T2) = {pol} by
BORSUK_1:40,XXREAL_1:174,418;
A20: T2 is compact by HEINE:4;
reconsider f as Function of I[01], T by A18,A9,FUNCT_2:def 1,RELSET_1:4;
P is continuous & Q is continuous by A1,A2,Def2;
then reconsider f as continuous Function of I[01], T by A8,A14,A19,A10,A20,
COMPTS_1:20,TOPMETR:20;
1 in { r : 1/2 <= r & r <= 1 };
then 1 in dom E2 by A4,A16,RCOMP_1:def 1;
then
A21: f.1 = E2.1 by FUNCT_4:13
.= Q.(2*1-1) by A5
.= c by A2,Def2;
then a,c are_connected by A17;
then reconsider f as Path of a, c by A17,A21,Def2;
for t being Point of I[01] holds ( t <= 1/2 implies f.t = P.(2*t) ) &
( 1/2 <= t implies f.t = Q.(2*t-1) )
proof
let t be Point of I[01];
A22: 0 <= t by Lm1;
thus t <= 1/2 implies f.t = P.(2*t)
proof
assume
A23: t <= 1/2;
then t in { r : 0 <= r & r <= 1/2 } by A22;
then
A24: t in [.0,1/2.] by RCOMP_1:def 1;
per cases;
suppose
A25: t <> 1/2;
not t in dom E2
proof
assume t in dom E2;
then t in [.0,1/2.] /\ [.1/2,1.] by A4,A16,A24,XBOOLE_0:def 4;
then t in {1/2} by XXREAL_1:418;
hence thesis by A25,TARSKI:def 1;
end;
then f.t = E1.t by FUNCT_4:11
.= P.(2*t) by A11,A22,A23;
hence thesis;
end;
suppose
A26: t = 1/2;
1/2 in { r : 1/2 <= r & r <= 1 };
then 1/2 in [.1/2, 1.] by RCOMP_1:def 1;
then 1/2 in the carrier of Closed-Interval-TSpace(1/2,1) by
TOPMETR:18;
then t in dom E2 by A26,FUNCT_2:def 1,TOPMETR:20;
then f.t = E1.t by A14,A26,FUNCT_4:13
.= P.(2*t) by A11,A22,A23;
hence thesis;
end;
end;
A27: t <= 1 by Lm1;
thus 1/2 <= t implies f.t = Q.(2*t-1)
proof
assume
A28: 1/2 <= t;
then t in { r : 1/2 <= r & r <= 1 } by A27;
then t in [.1/2,1.] by RCOMP_1:def 1;
then f.t = E2.t by A4,A16,FUNCT_4:13
.= Q.(2*t-1) by A5,A27,A28;
hence thesis;
end;
end;
hence thesis;
end;
uniqueness
proof
let A, B be Path of a, c such that
A29: for t being Point of I[01] holds ( t <= 1/2 implies A.t = P.(2*t)
) & ( 1/2 <= t implies A.t = Q.(2*t-1) ) and
A30: for t being Point of I[01] holds ( t <= 1/2 implies B.t = P.(2*t)
) & ( 1/2 <= t implies B.t = Q.(2*t-1) );
A31: for x be object st x in dom A holds A.x = B.x
proof
let x be object;
assume
A32: x in dom A;
then reconsider y = x as Point of I[01];
x in the carrier of I[01] by A32;
then x in { r : 0 <= r & r <= 1 } by BORSUK_1:40,RCOMP_1:def 1;
then consider r9 being Real such that
A33: r9 = x and
0 <= r9 and
r9 <= 1;
per cases;
suppose
A34: r9 <= 1/2;
then A.y = P.(2*r9) by A29,A33
.= B.y by A30,A33,A34;
hence thesis;
end;
suppose
A35: 1/2 < r9;
then A.y = Q.(2*r9-1) by A29,A33
.= B.y by A30,A33,A35;
hence thesis;
end;
end;
dom B = the carrier of I[01] by FUNCT_2:def 1;
then dom A = dom B by FUNCT_2:def 1;
hence thesis by A31,FUNCT_1:2;
end;
end;
registration
let T be non empty TopSpace;
let a be Point of T;
cluster constant for Path of a, a;
existence
proof
set IT = I[01] --> a;
A1: IT.0 = a & IT.1 = a by BORSUK_1:def 14,def 15,FUNCOP_1:7;
a,a are_connected;
then reconsider IT as Path of a, a by A1,Def2;
for n1,n2 being object st n1 in dom IT & n2 in dom IT holds IT.n1=IT.n2
proof
let n1,n2 be object;
assume that
A2: n1 in dom IT and
A3: n2 in dom IT;
IT.n1 = a by A2,FUNCOP_1:7
.= IT.n2 by A3,FUNCOP_1:7;
hence thesis;
end;
then IT is constant by FUNCT_1:def 10;
hence thesis;
end;
end;
::$CT
theorem
for T being non empty TopSpace, a being Point of T, P being constant
Path of a, a holds P = I[01] --> a
proof
let T be non empty TopSpace, a be Point of T, P be constant Path of a, a;
set IT = I[01] --> a;
A1: dom P = the carrier of I[01] by FUNCT_2:def 1;
A2: a,a are_connected;
A3: for x be object st x in the carrier of I[01] holds P.x = IT.x
proof
0 in { r : 0 <= r & r <= 1 };
then
A4: 0 in the carrier of I[01] by BORSUK_1:40,RCOMP_1:def 1;
let x be object;
assume
A5: x in the carrier of I[01];
P.0 = a by A2,Def2;
then P.x = a by A1,A5,A4,FUNCT_1:def 10
.= IT.x by A5,FUNCOP_1:7;
hence thesis;
end;
dom IT = the carrier of I[01] by FUNCT_2:def 1;
hence thesis by A1,A3,FUNCT_1:2;
end;
theorem Th5:
for T being non empty TopSpace, a being Point of T, P being
constant Path of a, a holds P + P = P
proof
let T be non empty TopSpace, a be Point of T, P be constant Path of a, a;
A1: the carrier of I[01] = dom P by FUNCT_2:def 1;
A2: for x be object st x in the carrier of I[01] holds P.x = (P+P).x
proof
let x be object;
assume
A3: x in the carrier of I[01];
then reconsider p = x as Point of I[01];
x in { r : 0 <= r & r <= 1 } by A3,BORSUK_1:40,RCOMP_1:def 1;
then consider r being Real such that
A4: r = x and
A5: 0 <= r and
A6: r <= 1;
per cases;
suppose
A7: r < 1/2;
then
A8: r * 2 < 1/2 * 2 by XREAL_1:68;
2 * r >= 0 by A5,XREAL_1:127;
then 2 * r in { e where e is Real: 0 <= e & e <= 1 } by A8;
then 2 * r in the carrier of I[01] by BORSUK_1:40,RCOMP_1:def 1;
then P.(2*r) = P.p by A1,FUNCT_1:def 10;
hence thesis by A4,A7,Def5;
end;
suppose
A9: r >= 1/2;
then r * 2 >= 1/2 * 2 by XREAL_1:64;
then 2 * r >= 1 + 0;
then
A10: 2 * r - 1 >= 0 by XREAL_1:19;
r * 2 <= 1 * 2 by A6,XREAL_1:64;
then 2 * r - 1 <= 2 - 1 by XREAL_1:13;
then 2 * r - 1 in { e where e is Real : 0 <= e & e <= 1 } by A10;
then 2 * r - 1 in the carrier of I[01] by BORSUK_1:40,RCOMP_1:def 1;
then P.(2*r-1) = P.p by A1,FUNCT_1:def 10;
hence thesis by A4,A9,Def5;
end;
end;
dom (P + P) = the carrier of I[01] by FUNCT_2:def 1;
hence thesis by A1,A2,FUNCT_1:2;
end;
registration
let T be non empty TopSpace, a be Point of T, P be constant Path of a, a;
cluster P + P -> constant;
coherence by Th5;
end;
definition
let T be non empty TopSpace;
let a, b be Point of T;
let P be Path of a, b;
assume
A1: a,b are_connected;
func - P -> Path of b, a means
:Def6:
for t being Point of I[01] holds it.t = P.(1-t);
existence
proof
set e = L[01]((0,1)(#),(#)(0,1));
reconsider f = P * e as Function of I[01], T by TOPMETR:20;
A2: for t being Point of I[01] holds f.t = P.(1-t)
proof
let t be Point of I[01];
reconsider ee = t as Point of Closed-Interval-TSpace (0,1) by TOPMETR:20;
A3: (0,1)(#) = 1 & (#)(0,1) = 0 by TREAL_1:def 1,def 2;
t in the carrier of Closed-Interval-TSpace (0,1) by TOPMETR:20;
then t in dom e by FUNCT_2:def 1;
then f.t = P.(e.ee) by FUNCT_1:13
.= P.((0-1)*t + 1) by A3,TREAL_1:7
.= P.(1 - 1*t);
hence thesis;
end;
0 in { r : 0 <= r & r <= 1 };
then 0 in [.0,1.] by RCOMP_1:def 1;
then 0 in the carrier of Closed-Interval-TSpace (0,1) by TOPMETR:18;
then
A4: 0 in dom e by FUNCT_2:def 1;
e.0 = e.(#)(0,1) by TREAL_1:def 1
.= (0,1)(#) by TREAL_1:9
.= 1 by TREAL_1:def 2;
then
A5: f.0 = P.1 by A4,FUNCT_1:13
.= b by A1,Def2;
1 in { r : 0 <= r & r <= 1 };
then 1 in [.0,1.] by RCOMP_1:def 1;
then 1 in the carrier of Closed-Interval-TSpace (0,1) by TOPMETR:18;
then
A6: 1 in dom e by FUNCT_2:def 1;
e.1 = e.(0,1)(#) by TREAL_1:def 2
.= (#)(0,1) by TREAL_1:9
.= 0 by TREAL_1:def 1;
then
A7: f.1 = P.0 by A6,FUNCT_1:13
.= a by A1,Def2;
A8: P is continuous & e is continuous Function of Closed-Interval-TSpace(
0,1), Closed-Interval-TSpace(0,1) by A1,Def2,TREAL_1:8;
then b, a are_connected by A5,A7,TOPMETR:20;
then reconsider f as Path of b, a by A5,A7,A8,Def2,TOPMETR:20;
take f;
thus thesis by A2;
end;
uniqueness
proof
let R, Q be Path of b, a such that
A9: for t being Point of I[01] holds R.t = P.(1-t) and
A10: for t being Point of I[01] holds Q.t = P.(1-t);
A11: for x be object st x in the carrier of I[01] holds R.x = Q.x
proof
let x be object;
assume x in the carrier of I[01];
then reconsider x9 = x as Point of I[01];
R.x9 = P.(1-x9) by A9
.= Q.x9 by A10;
hence thesis;
end;
dom R = the carrier of I[01] & the carrier of I[01] = dom Q by
FUNCT_2:def 1;
hence thesis by A11,FUNCT_1:2;
end;
end;
Lm4: for r be Real st 0 <= r & r <= 1 holds 0 <= 1-r & 1-r <= 1
proof
let r be Real;
assume 0 <= r & r <= 1;
then 1-1 <= 1-r & 1-r <= 1-0 by XREAL_1:13;
hence thesis;
end;
Lm5: for r being Real st r in the carrier of I[01] holds 1-r in the carrier of
I[01]
proof
let r be Real;
assume r in the carrier of I[01];
then 0 <= r & r <= 1 by Lm1;
then 0 <= 1-r & 1-r <= 1 by Lm4;
hence thesis by Lm1;
end;
theorem Th6:
for T being non empty TopSpace, a being Point of T, P being
constant Path of a, a holds - P = P
proof
let T be non empty TopSpace, a be Point of T, P be constant Path of a, a;
A1: dom P = the carrier of I[01] by FUNCT_2:def 1;
A2: for x be object st x in the carrier of I[01] holds P.x = (-P).x
proof
let x be object;
assume
A3: x in the carrier of I[01];
then reconsider x2 = x as Real;
reconsider x3 = 1 - x2 as Point of I[01] by A3,Lm5;
(-P).x = P.x3 by A3,Def6
.= P.x by A1,A3,FUNCT_1:def 10;
hence thesis;
end;
dom (-P) = the carrier of I[01] by FUNCT_2:def 1;
hence thesis by A1,A2,FUNCT_1:2;
end;
registration
let T be non empty TopSpace, a be Point of T, P be constant Path of a, a;
cluster - P -> constant;
coherence by Th6;
end;
begin :: The product of two topological spaces
theorem Th7:
for X, Y being non empty TopSpace for A being Subset-Family of Y
for f being Function of X, Y holds f"(union A) = union (f"A)
proof
let X, Y be non empty TopSpace, A be Subset-Family of Y, f be Function of X,
Y;
thus f"(union A) c= union (f"A)
proof
reconsider uA = union A as Subset of Y;
let x be object;
assume
A1: x in f"(union A);
then f.x in uA by FUNCT_2:38;
then consider YY being set such that
A2: f.x in YY and
A3: YY in A by TARSKI:def 4;
reconsider fY = f"YY as Subset of X;
A4: fY in f"A by A3,FUNCT_2:def 9;
x in f"YY by A1,A2,FUNCT_2:38;
hence thesis by A4,TARSKI:def 4;
end;
let x be object;
assume x in union (f"A);
then consider YY be set such that
A5: x in YY and
A6: YY in f"A by TARSKI:def 4;
x in the carrier of X by A5,A6;
then
A7: x in dom f by FUNCT_2:def 1;
reconsider B1 = YY as Subset of X by A6;
consider B being Subset of Y such that
A8: B in A and
A9: B1 = f"B by A6,FUNCT_2:def 9;
f.x in B by A5,A9,FUNCT_1:def 7;
then f.x in union A by A8,TARSKI:def 4;
hence thesis by A7,FUNCT_1:def 7;
end;
definition
let S1, S2, T1, T2 be non empty TopSpace;
let f be Function of S1, S2, g be Function of T1, T2;
redefine func [:f, g:] -> Function of [:S1, T1:], [:S2, T2:]; :: redefines [: (FUNCT_3, definition)
coherence
proof
set h = [:f, g:];
rng h c= [:the carrier of S2, the carrier of T2:];
then
A1: rng h c= the carrier of [:S2, T2:] by BORSUK_1:def 2;
dom h = [:the carrier of S1, the carrier of T1:] by FUNCT_2:def 1
.= the carrier of [:S1, T1:] by BORSUK_1:def 2;
hence thesis by A1,FUNCT_2:def 1,RELSET_1:4;
end;
end;
theorem Th8:
for S1, S2, T1, T2 be non empty TopSpace, f be continuous
Function of S1, T1, g be continuous Function of S2, T2, P1, P2 being Subset of
[:T1, T2:] holds (P2 in Base-Appr P1 implies [:f,g:]"P2 is open)
proof
let S1, S2, T1, T2 be non empty TopSpace, f be continuous Function of S1, T1
, g be continuous Function of S2, T2, P1, P2 be Subset of [:T1, T2:];
assume P2 in Base-Appr P1;
then consider X11 be Subset of T1, Y11 be Subset of T2 such that
A1: P2 = [:X11,Y11:] and
[:X11,Y11:] c= P1 and
A2: X11 is open and
A3: Y11 is open;
[#]T1 <> {};
then
A4: f"X11 is open by A2,TOPS_2:43;
[#]T2 <> {};
then
A5: g"Y11 is open by A3,TOPS_2:43;
[:f,g:]"P2 = [:f"X11, g"Y11:] by A1,FUNCT_3:73;
hence thesis by A4,A5,BORSUK_1:6;
end;
theorem Th9:
for S1, S2, T1, T2 be non empty TopSpace, f be continuous
Function of S1, T1, g be continuous Function of S2, T2, P2 being Subset of [:T1
, T2:] holds (P2 is open implies [:f,g:]"P2 is open)
proof
let S1, S2, T1, T2 be non empty TopSpace, f be continuous Function of S1, T1
, g be continuous Function of S2, T2, P2 be Subset of [:T1, T2:];
reconsider Kill = [:f,g:]"Base-Appr P2 as Subset-Family of [:S1, S2:];
for P being Subset of [:S1, S2:] holds P in Kill implies P is open
proof
let P be Subset of [:S1, S2:];
assume P in Kill;
then
ex B being Subset of [:T1, T2:] st B in Base-Appr P2 & P = [:f,g:]"B by
FUNCT_2:def 9;
hence thesis by Th8;
end;
then
A1: Kill is open by TOPS_2:def 1;
assume P2 is open;
then P2 = union Base-Appr P2 by BORSUK_1:13;
then
[:f,g:]"(P2 qua Subset of [:T1, T2:]) = union ([:f,g:]"Base-Appr P2) by Th7;
hence thesis by A1,TOPS_2:19;
end;
registration
let S1, S2, T1, T2 be non empty TopSpace,
f be continuous Function of S1, T1, g be continuous Function of S2, T2;
cluster [:f,g:] -> continuous for Function of [:S1,S2:], [:T1,T2:];
coherence
proof
[#][:T1,T2:] <> {} & for P1 be Subset of [:T1, T2:] st P1 is open holds
[:f, g:]"P1 is open by Th9;
hence thesis by TOPS_2:43;
end;
end;
registration
let T1, T2 be T_0 TopSpace;
cluster [:T1, T2:] -> T_0;
coherence
proof
set T = [:T1,T2:];
per cases;
suppose T1 is empty or T2 is empty;
hence thesis;
end;
suppose that
A1: T1 is non empty and
A2: T2 is non empty;
A3: the carrier of T is non empty by A1,A2;
now
let p,q be Point of T;
assume
A4: p <> q;
q in the carrier of T by A3;
then q in [:the carrier of T1, the carrier of T2:] by BORSUK_1:def 2;
then consider z,v be object such that
A5: z in the carrier of T1 and
A6: v in the carrier of T2 and
A7: q = [z,v] by ZFMISC_1:def 2;
p in the carrier of T by A3;
then p in [:the carrier of T1, the carrier of T2:] by BORSUK_1:def 2;
then consider x,y be object such that
A8: x in the carrier of T1 and
A9: y in the carrier of T2 and
A10: p = [x,y] by ZFMISC_1:def 2;
reconsider y, v as Point of T2 by A9,A6;
reconsider x, z as Point of T1 by A8,A5;
per cases;
suppose
x <> z;
then consider V1 being Subset of T1 such that
A11: V1 is open and
A12: x in V1 & not z in V1 or z in V1 & not x in V1 by A1,T_0TOPSP:def 7;
set X = [:V1, [#]T2:];
A13: now
per cases by A12;
suppose
x in V1 & not z in V1;
hence p in X & not q in X or q in X & not p in X by A9,A10,A7,
ZFMISC_1:87;
end;
suppose
z in V1 & not x in V1;
hence p in X & not q in X or q in X & not p in X by A10,A6,A7,
ZFMISC_1:87;
end;
end;
X is open by A11,BORSUK_1:6;
hence ex X being Subset of T st X is open & ( p in X & not q in X or q
in X & not p in X ) by A13;
end;
suppose
x = z;
then consider V1 being Subset of T2 such that
A14: V1 is open and
A15: y in V1 & not v in V1 or v in V1 & not y in V1 by A4,A10,A7,A2,
T_0TOPSP:def 7;
set X = [:[#]T1, V1:];
A16: now
per cases by A15;
suppose
y in V1 & not v in V1;
hence p in X & not q in X or q in X & not p in X by A8,A10,A7,
ZFMISC_1:87;
end;
suppose
v in V1 & not y in V1;
hence p in X & not q in X or q in X & not p in X by A10,A5,A7,
ZFMISC_1:87;
end;
end;
X is open by A14,BORSUK_1:6;
hence ex X being Subset of T st X is open & ( p in X & not q in X or q
in X & not p in X ) by A16;
end;
end;
hence thesis;
end;
end;
end;
registration
let T1, T2 be T_1 TopSpace;
cluster [:T1, T2:] -> T_1;
coherence
proof
set T = [:T1, T2:];
per cases;
suppose T1 is empty or T2 is empty;
hence thesis;
end;
suppose T1 is non empty & T2 is non empty;
then
A1: the carrier of [:T1,T2:] is non empty;
let p,q be Point of T;
assume
A2: p <> q;
q in the carrier of T by A1;
then q in [:the carrier of T1, the carrier of T2:] by BORSUK_1:def 2;
then consider z,v be object such that
A3: z in the carrier of T1 and
A4: v in the carrier of T2 and
A5: q = [z,v] by ZFMISC_1:def 2;
p in the carrier of T by A1;
then p in [:the carrier of T1, the carrier of T2:] by BORSUK_1:def 2;
then consider x,y be object such that
A6: x in the carrier of T1 and
A7: y in the carrier of T2 and
A8: p = [x,y] by ZFMISC_1:def 2;
reconsider y, v as Point of T2 by A7,A4;
reconsider x, z as Point of T1 by A6,A3;
per cases;
suppose
x <> z;
then consider Y, V be Subset of T1 such that
A9: Y is open & V is open and
A10: x in Y and
A11: not z in Y and
A12: z in V and
A13: not x in V by URYSOHN1:def 7;
set X = [:Y, [#]T2:], Z = [:V, [#]T2:];
A14: ( not q in X)& not p in Z by A8,A5,A11,A13,ZFMISC_1:87;
A15: X is open & Z is open by A9,BORSUK_1:6;
p in X & q in Z by A7,A8,A4,A5,A10,A12,ZFMISC_1:87;
hence thesis by A15,A14;
end;
suppose
x = z;
then consider Y, V be Subset of T2 such that
A16: Y is open & V is open and
A17: y in Y and
A18: not v in Y and
A19: v in V and
A20: not y in V by A2,A8,A5,URYSOHN1:def 7;
reconsider Y, V as Subset of T2;
set X = [:[#]T1, Y:], Z = [:[#]T1, V:];
A21: ( not p in Z)& not q in X by A8,A5,A18,A20,ZFMISC_1:87;
A22: X is open & Z is open by A16,BORSUK_1:6;
p in X & q in Z by A6,A8,A3,A5,A17,A19,ZFMISC_1:87;
hence thesis by A22,A21;
end;
end;
end;
end;
registration
let T1, T2 be T_2 TopSpace;
cluster [:T1, T2:] -> T_2;
coherence
proof
set T = [:T1, T2:];
per cases;
suppose T1 is empty or T2 is empty;
hence thesis;
end;
suppose T1 is non empty & T2 is non empty;
then
A1: the carrier of T is non empty;
let p,q be Point of T;
assume
A2: p <> q;
q in the carrier of T by A1;
then q in [:the carrier of T1, the carrier of T2:] by BORSUK_1:def 2;
then consider z,v be object such that
A3: z in the carrier of T1 and
A4: v in the carrier of T2 and
A5: q = [z,v] by ZFMISC_1:def 2;
p in the carrier of T by A1;
then p in [:the carrier of T1, the carrier of T2:] by BORSUK_1:def 2;
then consider x,y be object such that
A6: x in the carrier of T1 and
A7: y in the carrier of T2 and
A8: p = [x,y] by ZFMISC_1:def 2;
reconsider y, v as Point of T2 by A7,A4;
reconsider x, z as Point of T1 by A6,A3;
per cases;
suppose
x <> z;
then consider Y, V be Subset of T1 such that
A9: Y is open & V is open and
A10: x in Y & z in V and
A11: Y misses V by PRE_TOPC:def 10;
reconsider Y, V as Subset of T1;
reconsider X = [:Y, [#]T2:], Z = [:V, [#]T2:] as Subset of T;
A12: X misses Z by A11,ZFMISC_1:104;
A13: X is open & Z is open by A9,BORSUK_1:6;
p in X & q in Z by A7,A8,A4,A5,A10,ZFMISC_1:87;
hence thesis by A13,A12;
end;
suppose
x = z;
then consider Y, V be Subset of T2 such that
A14: Y is open & V is open and
A15: y in Y & v in V and
A16: Y misses V by A2,A8,A5,PRE_TOPC:def 10;
reconsider Y, V as Subset of T2;
reconsider X = [:[#]T1, Y:], Z = [:[#]T1, V:] as Subset of T;
A17: X misses Z by A16,ZFMISC_1:104;
A18: X is open & Z is open by A14,BORSUK_1:6;
p in X & q in Z by A6,A8,A3,A5,A15,ZFMISC_1:87;
hence thesis by A18,A17;
end;
end;
end;
end;
registration
cluster I[01] -> compact T_2;
coherence
proof
I[01] = TopSpaceMetr (Closed-Interval-MSpace(0,1)) by TOPMETR:20,def 7;
hence thesis by HEINE:4,PCOMPS_1:34,TOPMETR:20;
end;
end;
definition
let T be non empty TopStruct;
let a, b be Point of T;
let P, Q be Path of a, b;
pred P, Q are_homotopic means
ex f being Function of [:I[01],I[01]:], T st f
is continuous & for t being Point of I[01] holds f.(t,0) = P.t & f.(t,1) = Q.t
& f.(0,t) = a & f.(1,t) = b;
symmetry
proof
id the carrier of I[01] = id I[01];
then reconsider
fA = id the carrier of I[01] as continuous Function of I[01],
I[01];
set LL = L[01]((0,1)(#),(#)(0,1));
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;
given f being Function of [:I[01],I[01]:], T such that
A1: f is continuous and
A2: for s being Point of I[01] holds f.(s,0) = P.s & f.(s,1) = Q.s & f
.( 0,s) = a & f.(1,s) = b;
set F = [:fA, fB:];
reconsider ff=f * F as Function of [:I[01],I[01]:], T;
A3: dom L[01]((0,1)(#),(#)(0,1)) = the carrier of I[01] by FUNCT_2:def 1
,TOPMETR:20;
A4: for s being Point of I[01] holds ff.(s,0) = Q.s & ff.(s,1) = P.s
proof
let s be Point of I[01];
A5: for t being Point of I[01], t9 being Real st t = t9
holds LL.t = 1- t9
proof
let t be Point of I[01], t9 be Real;
assume
A6: t = t9;
reconsider ee = t as Point of Closed-Interval-TSpace (0,1) by
TOPMETR:20;
A7: (0,1)(#) = 1 & (#)(0,1) = 0 by TREAL_1:def 1,def 2;
LL.t = LL.ee .= ((0-1)*t9 + 1) by A6,A7,TREAL_1:7
.= (1 - 1*t9);
hence thesis;
end;
A8: dom id the carrier of I[01] = the carrier of I[01];
A9: dom F = [:dom id the carrier of I[01], dom L[01]((0,1)(#),(#)(0,1))
:] by FUNCT_3:def 8;
A10: 1 in dom L[01]((0,1)(#),(#)(0,1)) by A3,Lm1;
then
A11: [s,1] in dom F by A9,ZFMISC_1:87;
A12: 0 in dom LL by A3,Lm1;
then
A13: [s,0] in dom F by A9,ZFMISC_1:87;
F.(s,1) = [(id the carrier of I[01]).s,(L[01]((0,1)(#),(#)(0,1))).1
] by A8,A10,FUNCT_3:def 8
.= [s,LL.1[01]]
.= [s,1 - 1] by A5
.= [s,0];
then
A14: ff.(s,1) = f.(s,0) by A11,FUNCT_1:13
.= P.s by A2;
F.(s,0) = [(id the carrier of I[01]).s,LL.0] by A8,A12,FUNCT_3:def 8
.= [s, LL.0[01]]
.= [s, 1 - 0] by A5
.= [s, 1];
then ff.(s,0) = f.(s,1) by A13,FUNCT_1:13
.= Q.s by A2;
hence thesis by A14;
end;
A15: for t being Point of I[01] holds ff.(0,t) = a & ff.(1,t) = b
proof
let t be Point of I[01];
reconsider tt = t as Real;
for t being Point of I[01], t9 being Real st t = t9 holds LL.t = 1- t9
proof
let t be Point of I[01], t9 be Real;
assume
A16: t = t9;
reconsider ee = t as Point of Closed-Interval-TSpace (0,1) by
TOPMETR:20;
A17: (0,1)(#) = 1 & (#)(0,1) = 0 by TREAL_1:def 1,def 2;
LL.t = LL.ee .= (0-1)*t9 + 1 by A16,A17,TREAL_1:7
.= 1 - 1*t9;
hence thesis;
end;
then
A18: (L[01]((0,1)(#),(#)(0,1))).t = 1 - tt;
reconsider t9 = 1 - tt as Point of I[01] by Lm5;
A19: dom L[01]((0,1)(#),(#)(0,1)) = the carrier of I[01] by FUNCT_2:def 1
,TOPMETR:20;
A20: 0 in dom id the carrier of I[01] by Lm1;
A21: dom F = [:dom id the carrier of I[01], dom L[01]((0,1)(#),(#)(0,1))
:] by FUNCT_3:def 8;
then
A22: [0,t] in dom F by A19,A20,ZFMISC_1:87;
A23: 1 in dom id the carrier of I[01] by Lm1;
then
A24: [1,t] in dom F by A19,A21,ZFMISC_1:87;
F.(1,t) = [(id the carrier of I[01]).1,(L[01]((0,1)(#),(#)(0,1))).t
] by A19,A23,FUNCT_3:def 8
.= [1,1 - tt] by A18,A23,FUNCT_1:18;
then
A25: ff.(1,t) = f.(1,t9) by A24,FUNCT_1:13
.= b by A2;
F.(0,t) = [(id the carrier of I[01]).0,(L[01]((0,1)(#),(#)(0,1 ))).
t ] by A19,A20,FUNCT_3:def 8
.= [0,1 - tt] by A18,A20,FUNCT_1:18;
then ff.(0,t) = f.(0,t9) by A22,FUNCT_1:13
.= a by A2;
hence thesis by A25;
end;
ff is continuous by A1,TOPS_2:46;
hence thesis by A4,A15;
end;
end;
::$CT
theorem Th10:
for T being non empty TopSpace, a, b being Point of T, P being
Path of a, b st a,b are_connected holds P, P are_homotopic
proof
let T be non empty TopSpace;
let a, b be Point of T;
let P be Path of a, b;
defpred Z[object, object] means $2 = P.($1`1);
A1: for x be object st x in [:the carrier of I[01], the carrier of I[01]:]
ex y be object st y in the carrier of T & Z[x,y]
proof
let x be object;
assume x in [:the carrier of I[01], the carrier of I[01]:];
then x`1 in the carrier of I[01] by MCART_1:10;
hence thesis by FUNCT_2:5;
end;
consider f being Function of [:the carrier of I[01], the carrier of I[01]:],
the carrier of T such that
A2: for x being object st x in [:the carrier of I[01], the carrier of I[01]
:] holds Z[x, f.x] from FUNCT_2:sch 1(A1);
the carrier of [:I[01],I[01]:] = [:the carrier of I[01], the carrier of
I[01]:] by BORSUK_1:def 2;
then reconsider
f as Function of the carrier of [:I[01],I[01]:], the carrier of T;
reconsider f as Function of [:I[01],I[01]:], T;
assume
A3: a,b are_connected;
A4: for t being Point of I[01] holds f.(0,t) = a & f.(1,t) = b
proof
let t be Point of I[01];
set t0 = [0,t], t1 = [1,t];
0 in the carrier of I[01] by Lm1;
then t0 in [:the carrier of I[01], the carrier of I[01]:] by ZFMISC_1:87;
then
A5: f.t0 = P.(t0`1) by A2;
1 in the carrier of I[01] by Lm1;
then t1 in [:the carrier of I[01], the carrier of I[01]:] by ZFMISC_1:87;
then
A6: f.t1 = P.(t1`1) by A2;
P.0 = a & P.1 = b by A3,Def2;
hence thesis by A5,A6;
end;
A7: for W being Point of [:I[01], I[01]:], G being a_neighborhood of f.W ex
H being a_neighborhood of W st f.:H c= G
proof
let W be Point of [:I[01], I[01]:], G be a_neighborhood of f.W;
W in the carrier of [:I[01], I[01]:];
then
A8: W in [:the carrier of I[01], the carrier of I[01]:] by BORSUK_1:def 2;
then reconsider W1 = W`1 as Point of I[01] by MCART_1:10;
A9: ex x,y be object st [x,y] = W by A8,RELAT_1:def 1;
reconsider G9 = G as a_neighborhood of P.W1 by A2,A8;
the carrier of I[01] c= the carrier of I[01];
then reconsider AI = the carrier of I[01] as Subset of I[01];
AI = [#]I[01];
then Int AI = the carrier of I[01] by TOPS_1:15;
then
A10: W`2 in Int AI by A8,MCART_1:10;
P is continuous by A3,Def2;
then consider H be a_neighborhood of W1 such that
A11: P.:H c= G9;
set HH = [:H, the carrier of I[01]:];
HH c= [:the carrier of I[01], the carrier of I[01]:] by ZFMISC_1:95;
then reconsider HH as Subset of [:I[01], I[01]:] by BORSUK_1:def 2;
W1 in Int H & Int HH = [:Int H, Int AI:] by BORSUK_1:7,CONNSP_2:def 1;
then W in Int HH by A9,A10,ZFMISC_1:def 2;
then reconsider HH as a_neighborhood of W by CONNSP_2:def 1;
take HH;
f.:HH c= G
proof
let a be object;
assume a in f.:HH;
then consider b be object such that
A12: b in dom f and
A13: b in HH and
A14: a = f.b by FUNCT_1:def 6;
reconsider b as Point of [:I[01], I[01]:] by A12;
A15: dom P = the carrier of I[01] & b`1 in H by A13,FUNCT_2:def 1,MCART_1:10;
dom f = [:the carrier of I[01], the carrier of I[01]:] by FUNCT_2:def 1;
then f.b = P.(b`1) by A2,A12;
then f.b in P.:H by A15,FUNCT_1:def 6;
hence thesis by A11,A14;
end;
hence thesis;
end;
take f;
for s being Point of I[01] holds f.(s,0) = P.s & f.(s,1) = P.s
proof
let s be Point of I[01];
reconsider s0 = [s,0], s1 = [s,1] as set;
1 in the carrier of I[01] by Lm1;
then s1 in [:the carrier of I[01], the carrier of I[01]:] by ZFMISC_1:87;
then
A16: Z[s1, f.s1] by A2;
0 in the carrier of I[01] by Lm1;
then s0 in [:the carrier of I[01], the carrier of I[01]:] by ZFMISC_1:87;
then Z[s0, f.s0] by A2;
hence thesis by A16;
end;
hence thesis by A7,A4;
end;
definition
let T be non empty pathwise_connected TopSpace;
let a, b be Point of T;
let P, Q be Path of a, b;
redefine pred P, Q are_homotopic; :: redefines are_homotopic (BORSUK_2, definition)
reflexivity by Th10,Def3;
end;
theorem
for G being non empty TopSpace, w1,w2,w3 being Point of G, h1,h2 being
Function of I[01],G st h1 is continuous & w1=h1.0 & w2=h1.1 & h2 is continuous
& w2=h2.0 & w3=h2.1 holds ex h3 being Function of I[01],G st h3 is continuous &
w1=h3.0 & w3=h3.1 & rng h3 c= (rng h1) \/ (rng h2) by Lm3;
theorem
for T being non empty TopSpace,a,b,c being Point of T, G1 being Path
of a,b, G2 being Path of b,c st G1 is continuous & G2 is continuous & G1.0=a &
G1.1=b & G2.0=b & G2.1=c holds G1+G2 is continuous & (G1+G2).0=a & (G1+G2).1=c
proof
let T be non empty TopSpace,a,b,c be Point of T, G1 be Path of a,b, G2 be
Path of b,c;
assume
G1 is continuous & G2 is continuous & G1.0=a & G1.1=b & G2.0=b & G2. 1= c;
then
ex h being Function of I[01],T st h is continuous & h.0=a & h.1=c & rng
h c= (rng G1) \/ (rng G2) by Lm3;
then a,c are_connected;
hence thesis by Def2;
end;
registration
let T be non empty TopSpace;
cluster non empty compact connected for Subset of T;
existence
proof
take {the Element of T};
thus thesis;
end;
end;
:: Moved from BORSUK_5:11, AK, 20.02.2006
theorem Th13:
for T being non empty TopSpace, a, b being Point of T st (ex f
being Function of I[01], T st f is continuous & f.0 = a & f.1 = b) holds ex g
being Function of I[01], T st g is continuous & g.0 = b & g.1 = a
proof
set e = L[01]((0,1)(#),(#)(0,1));
let T be non empty TopSpace, a, b be Point of T;
given P being Function of I[01], T such that
A1: P is continuous and
A2: P.0 = a & P.1 = b;
set f = P * e;
reconsider f as Function of I[01], T by TOPMETR:20;
take f;
e is continuous Function of Closed-Interval-TSpace(0,1),
Closed-Interval-TSpace(0,1) by TREAL_1:8;
hence f is continuous by A1,TOPMETR:20;
A3: e.1 = e.(0,1)(#) by TREAL_1:def 2
.= (#)(0,1) by TREAL_1:9
.= 0 by TREAL_1:def 1;
1 in [. 0,1 .] by XXREAL_1:1;
then 1 in the carrier of Closed-Interval-TSpace (0,1) by TOPMETR:18;
then
A4: 1 in dom e by FUNCT_2:def 1;
0 in [. 0,1 .] by XXREAL_1:1;
then 0 in the carrier of Closed-Interval-TSpace (0,1) by TOPMETR:18;
then
A5: 0 in dom e by FUNCT_2:def 1;
e.0 = e.(#)(0,1) by TREAL_1:def 1
.= (0,1)(#) by TREAL_1:9
.= 1 by TREAL_1:def 2;
hence thesis by A2,A3,A5,A4,FUNCT_1:13;
end;
registration
cluster I[01] -> pathwise_connected;
coherence
proof
let a, b be Point of I[01];
per cases;
suppose
A1: a <= b;
then reconsider B = [. a, b .] as non empty Subset of I[01] by
BORSUK_1:40,XXREAL_1:1,XXREAL_2:def 12;
0 <= a & b <= 1 by BORSUK_1:43;
then
A2: Closed-Interval-TSpace(a,b) = I[01]|B by A1,TOPMETR:24;
the carrier of I[01]|B c= the carrier of I[01] by BORSUK_1:1;
then reconsider
g = L[01]((#)(a,b),(a,b)(#)) as Function of the carrier of
I[01], the carrier of I[01] by A2,FUNCT_2:7,TOPMETR:20;
reconsider g as Function of I[01], I[01];
take g;
thus g is continuous by A1,A2,PRE_TOPC:26,TOPMETR:20,TREAL_1:8;
0 = (#)(0,1) by TREAL_1:def 1;
hence g.0 = (#)(a,b) by A1,TREAL_1:9
.= a by A1,TREAL_1:def 1;
1 = (0,1)(#) by TREAL_1:def 2;
hence g.1 = (a,b)(#) by A1,TREAL_1:9
.= b by A1,TREAL_1:def 2;
end;
suppose
A3: b <= a;
then reconsider B = [. b, a .] as non empty Subset of I[01] by
BORSUK_1:40,XXREAL_1:1,XXREAL_2:def 12;
0 <= b & a <= 1 by BORSUK_1:43;
then
A4: Closed-Interval-TSpace(b,a) = I[01]|B by A3,TOPMETR:24;
the carrier of I[01]|B c= the carrier of I[01] by BORSUK_1:1;
then reconsider
g = L[01]((#)(b,a),(b,a)(#)) as Function of the carrier of
I[01], the carrier of I[01] by A4,FUNCT_2:7,TOPMETR:20;
reconsider g as Function of I[01], I[01];
0 = (#)(0,1) by TREAL_1:def 1;
then
A5: g.0 = (#)(b,a) by A3,TREAL_1:9
.= b by A3,TREAL_1:def 1;
1 = (0,1)(#) by TREAL_1:def 2;
then
A6: g.1 = (b,a)(#) by A3,TREAL_1:9
.= a by A3,TREAL_1:def 2;
A7: g is continuous by A3,A4,PRE_TOPC:26,TOPMETR:20,TREAL_1:8;
then b,a are_connected by A5,A6;
then reconsider P = g as Path of b, a by A7,A5,A6,Def2;
take -P;
ex t being Function of I[01], I[01] st t is continuous & t.0 = a &
t.1 = b by A7,A5,A6,Th13;
then a,b are_connected;
hence thesis by Def2;
end;
end;
end;