:: Introduction to Homotopy Theory :: by Adam Grabowski :: :: Received September 10, 1997 :: Copyright (c) 1997-2019 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; 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 :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:]; 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; 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;