:: Introduction to Homotopy Theory :: by Adam Grabowski :: :: Received September 10, 1997 :: Copyright (c) 1997-2017 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; begin :: Preliminaries reserve T,T1,T2,S for non empty TopSpace; scheme :: BORSUK_2:sch 1 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(); theorem :: BORSUK_2:1 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; registration let T be TopStruct; cluster id T -> open continuous; end; registration let T be TopStruct; cluster continuous one-to-one for Function of T, T; end; theorem :: BORSUK_2:2 for S, T being non empty TopSpace, f being Function of S, T st f is being_homeomorphism holds f" is open; begin :: Paths and arcwise connected spaces theorem :: BORSUK_2:3 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; definition let T be TopStruct, a,b be Point of T; pred a,b are_connected means :: BORSUK_2:def 1 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; end; definition let T be TopStruct; let a, b be Point of T; assume a, b are_connected; mode Path of a, b -> Function of I[01], T means :: BORSUK_2:def 2 it is continuous & it .0 = a & it.1 = b; end; registration let T be non empty TopSpace; let a be Point of T; cluster continuous for Path of a, a; end; definition let T be TopStruct; attr T is pathwise_connected means :: BORSUK_2:def 3 for a, b being Point of T holds a, b are_connected; end; registration cluster strict pathwise_connected non empty for TopSpace; end; definition let T be pathwise_connected TopStruct; let a, b be Point of T; redefine mode Path of a, b means :: BORSUK_2:def 4 it is continuous & it.0 = a & it.1 = b; end; registration let T be pathwise_connected TopStruct; let a, b be Point of T; cluster -> continuous for Path of a, b; end; reserve GY for non empty TopSpace, r,s for Real; registration cluster pathwise_connected -> connected for non empty TopSpace; end; begin 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 a,b are_connected and b,c are_connected; func P + Q -> Path of a, c means :: BORSUK_2:def 5 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) ); end; registration let T be non empty TopSpace; let a be Point of T; cluster constant for Path of a, a; end; ::\$CT theorem :: BORSUK_2:5 for T being non empty TopSpace, a being Point of T, P being constant Path of a, a holds P = I[01] --> a; theorem :: BORSUK_2:6 for T being non empty TopSpace, a being Point of T, P being constant Path of a, a holds P + P = P; registration let T be non empty TopSpace, a be Point of T, P be constant Path of a, a; cluster P + P -> constant; end; definition let T be non empty TopSpace; let a, b be Point of T; let P be Path of a, b; assume a,b are_connected; func - P -> Path of b, a means :: BORSUK_2:def 6 for t being Point of I[01] holds it.t = P.(1-t); end; theorem :: BORSUK_2:7 for T being non empty TopSpace, a being Point of T, P being constant Path of a, a holds - P = P; registration let T be non empty TopSpace, a be Point of T, P be constant Path of a, a; cluster - P -> constant; end; begin :: The product of two topological spaces theorem :: BORSUK_2:8 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); 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:]; end; theorem :: BORSUK_2:9 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); theorem :: BORSUK_2:10 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); 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:]; end; registration let T1, T2 be T_0 TopSpace; cluster [:T1, T2:] -> T_0; end; registration let T1, T2 be T_1 TopSpace; cluster [:T1, T2:] -> T_1; end; registration let T1, T2 be T_2 TopSpace; cluster [:T1, T2:] -> T_2; end; registration cluster I[01] -> compact T_2; 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 :: BORSUK_2:def 7 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; end; ::\$CT theorem :: BORSUK_2:12 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; 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; end; theorem :: BORSUK_2:13 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); theorem :: BORSUK_2:14 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; registration let T be non empty TopSpace; cluster non empty compact connected for Subset of T; end; :: Moved from BORSUK_5:11, AK, 20.02.2006 theorem :: BORSUK_2:15 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; registration cluster I[01] -> pathwise_connected; end;