:: TOPALG_2 semantic presentation begin registrationlet "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_convex1 :::"convex"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) "n" ")" ))); end; definitionlet "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "T" be ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set ($#k15_euclid :::"TOP-REAL"::: ) (Set (Const "n"))); attr "T" is :::"convex"::: means :: TOPALG_2:def 1 (Bool (Set ($#k2_struct_0 :::"[#]"::: ) "T") "is" ($#v1_convex1 :::"convex"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) "n" ")" )); end; :: deftheorem defines :::"convex"::: TOPALG_2:def 1 : (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "T")) "being" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n"))) "holds" (Bool "(" (Bool (Set (Var "T")) "is" ($#v1_topalg_2 :::"convex"::: ) ) "iff" (Bool (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "T"))) "is" ($#v1_convex1 :::"convex"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" )) ")" ))); registrationlet "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_topalg_2 :::"convex"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_borsuk_2 :::"pathwise_connected"::: ) for ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set ($#k15_euclid :::"TOP-REAL"::: ) "n"); end; registrationlet "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_pre_topc :::"strict"::: ) ($#v2_pre_topc :::"TopSpace-like"::: ) ($#v1_topalg_2 :::"convex"::: ) for ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set ($#k15_euclid :::"TOP-REAL"::: ) "n"); end; theorem :: TOPALG_2:1 (Bool "for" (Set (Var "X")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "X")) (Bool "for" (Set (Var "y1")) "," (Set (Var "y2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "Y")) (Bool "for" (Set (Var "f")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "y1")) "," (Set (Var "y2")) "st" (Bool (Bool (Set (Var "x1")) ($#r1_hidden :::"="::: ) (Set (Var "y1"))) & (Bool (Set (Var "x2")) ($#r1_hidden :::"="::: ) (Set (Var "y2"))) & (Bool (Set (Var "y1")) "," (Set (Var "y2")) ($#r1_borsuk_6 :::"are_connected"::: ) )) "holds" (Bool (Set (Var "f")) "is" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "x1")) "," (Set (Var "x2")))))))) ; definitionlet "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_topalg_2 :::"convex"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set ($#k15_euclid :::"TOP-REAL"::: ) (Set (Const "n"))); let "P", "Q" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set (Const "T")); func :::"ConvexHomotopy"::: "(" "P" "," "Q" ")" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set ($#k5_topmetr :::"I[01]"::: ) ) ($#k2_borsuk_1 :::":]"::: ) ) "," "T" means :: TOPALG_2:def 2 (Bool "for" (Set (Var "s")) "," (Set (Var "t")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) (Bool "for" (Set (Var "a1")) "," (Set (Var "b1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) "n" ")" ) "st" (Bool (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set "P" ($#k3_funct_2 :::"."::: ) (Set (Var "s")))) & (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set "Q" ($#k3_funct_2 :::"."::: ) (Set (Var "s"))))) "holds" (Bool (Set it ($#k1_binop_1 :::"."::: ) "(" (Set (Var "s")) "," (Set (Var "t")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Num 1) ($#k9_real_1 :::"-"::: ) (Set (Var "t")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "a1")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "t")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "b1")) ")" ))))); end; :: deftheorem defines :::"ConvexHomotopy"::: TOPALG_2:def 2 : (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_topalg_2 :::"convex"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n"))) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set (Var "T")) (Bool "for" (Set (Var "b5")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set ($#k5_topmetr :::"I[01]"::: ) ) ($#k2_borsuk_1 :::":]"::: ) ) "," (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k1_topalg_2 :::"ConvexHomotopy"::: ) "(" (Set (Var "P")) "," (Set (Var "Q")) ")" )) "iff" (Bool "for" (Set (Var "s")) "," (Set (Var "t")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) (Bool "for" (Set (Var "a1")) "," (Set (Var "b1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "a1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "P")) ($#k3_funct_2 :::"."::: ) (Set (Var "s")))) & (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "Q")) ($#k3_funct_2 :::"."::: ) (Set (Var "s"))))) "holds" (Bool (Set (Set (Var "b5")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "s")) "," (Set (Var "t")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Num 1) ($#k9_real_1 :::"-"::: ) (Set (Var "t")) ")" ) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "a1")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set "(" (Set (Var "t")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "b1")) ")" ))))) ")" ))))); theorem :: TOPALG_2:2 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_topalg_2 :::"convex"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n"))) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) "holds" (Bool (Set (Var "P")) "," (Set (Var "Q")) ($#r4_borsuk_2 :::"are_homotopic"::: ) ))))) ; registrationlet "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_topalg_2 :::"convex"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set ($#k15_euclid :::"TOP-REAL"::: ) (Set (Const "n"))); let "a", "b" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "T")); let "P", "Q" be ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Const "a")) "," (Set (Const "b")); cluster -> ($#v5_pre_topc :::"continuous"::: ) for ($#m1_borsuk_6 :::"Homotopy"::: ) "of" "P" "," "Q"; end; theorem :: TOPALG_2:3 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_topalg_2 :::"convex"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n"))) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "C")) "being" ($#m1_borsuk_2 :::"Loop":::) "of" (Set (Var "a")) "holds" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k5_topalg_1 :::"pi_1"::: ) "(" (Set (Var "T")) "," (Set (Var "a")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k4_topalg_1 :::"EqRel"::: ) "(" (Set (Var "T")) "," (Set (Var "a")) ")" ")" ) "," (Set (Var "C")) ")" ")" ) ($#k1_tarski :::"}"::: ) )))))) ; registrationlet "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_topalg_2 :::"convex"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set ($#k15_euclid :::"TOP-REAL"::: ) (Set (Const "n"))); let "a" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "T")); cluster (Set ($#k5_topalg_1 :::"FundamentalGroup"::: ) "(" "T" "," "a" ")" ) -> ($#v7_struct_0 :::"trivial"::: ) ; end; begin theorem :: TOPALG_2:4 (Bool "for" (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set ($#k1_jordan2b :::"|["::: ) (Set (Var "a")) ($#k1_jordan2b :::"]|"::: ) ) ($#k7_partfun1 :::"/."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Var "a")))) ; theorem :: TOPALG_2:5 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "b")))) "holds" (Bool (Set ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) ) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set "(" (Set "(" (Num 1) ($#k9_real_1 :::"-"::: ) (Set (Var "l")) ")" ) ($#k8_real_1 :::"*"::: ) (Set (Var "a")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "l")) ($#k8_real_1 :::"*"::: ) (Set (Var "b")) ")" ) ")" ) where l "is" ($#m1_subset_1 :::"Real":::) : (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "l"))) & (Bool (Set (Var "l")) ($#r1_xxreal_0 :::"<="::: ) (Num 1)) ")" ) "}" )) ; theorem :: TOPALG_2:6 (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set ($#k3_topmetr :::"R^1"::: ) ) "," (Set ($#k5_topmetr :::"I[01]"::: ) ) ($#k2_borsuk_1 :::":]"::: ) ) "," (Set ($#k3_topmetr :::"R^1"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k3_topmetr :::"R^1"::: ) ) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "holds" (Bool (Set (Set (Var "F")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 1) ($#k9_real_1 :::"-"::: ) (Set (Var "i")) ")" ) ($#k8_real_1 :::"*"::: ) (Set (Var "x"))))) ")" )) "holds" (Bool (Set (Var "F")) "is" ($#v5_pre_topc :::"continuous"::: ) )) ; theorem :: TOPALG_2:7 (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set ($#k3_topmetr :::"R^1"::: ) ) "," (Set ($#k5_topmetr :::"I[01]"::: ) ) ($#k2_borsuk_1 :::":]"::: ) ) "," (Set ($#k3_topmetr :::"R^1"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k3_topmetr :::"R^1"::: ) ) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "holds" (Bool (Set (Set (Var "F")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "i")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x"))))) ")" )) "holds" (Bool (Set (Var "F")) "is" ($#v5_pre_topc :::"continuous"::: ) )) ; registration cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) bbbadV1_MEMBERED() bbbadV2_MEMBERED() bbbadV3_MEMBERED() ($#v6_xxreal_2 :::"interval"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set ($#k3_topmetr :::"R^1"::: ) ))); end; registrationlet "T" be ($#v3_topmetr :::"real-membered"::: ) ($#l1_pre_topc :::"TopStruct"::: ) ; cluster bbbadV1_MEMBERED() bbbadV2_MEMBERED() bbbadV3_MEMBERED() ($#v6_xxreal_2 :::"interval"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" "T")); end; definitionlet "T" be ($#v3_topmetr :::"real-membered"::: ) ($#l1_pre_topc :::"TopStruct"::: ) ; attr "T" is :::"interval"::: means :: TOPALG_2:def 3 (Bool (Set ($#k2_struct_0 :::"[#]"::: ) "T") "is" ($#v6_xxreal_2 :::"interval"::: ) ); end; :: deftheorem defines :::"interval"::: TOPALG_2:def 3 : (Bool "for" (Set (Var "T")) "being" ($#v3_topmetr :::"real-membered"::: ) ($#l1_pre_topc :::"TopStruct"::: ) "holds" (Bool "(" (Bool (Set (Var "T")) "is" ($#v2_topalg_2 :::"interval"::: ) ) "iff" (Bool (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "T"))) "is" ($#v6_xxreal_2 :::"interval"::: ) ) ")" )); registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_pre_topc :::"strict"::: ) ($#v2_pre_topc :::"TopSpace-like"::: ) ($#v3_topmetr :::"real-membered"::: ) ($#v2_topalg_2 :::"interval"::: ) for ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set ($#k3_topmetr :::"R^1"::: ) ); end; definition:: original: :::"R^1"::: redefine func :::"R^1"::: -> ($#v2_topalg_2 :::"interval"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set ($#k3_topmetr :::"R^1"::: ) ); end; theorem :: TOPALG_2:8 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_topalg_2 :::"interval"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set ($#k2_topalg_2 :::"R^1"::: ) ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "holds" (Bool (Set ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) ) ($#r1_tarski :::"c="::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T")))))) ; registration cluster ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_topalg_2 :::"interval"::: ) -> ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_borsuk_2 :::"pathwise_connected"::: ) for ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set ($#k2_topalg_2 :::"R^1"::: ) ); end; theorem :: TOPALG_2:9 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "b")))) "holds" (Bool (Set ($#k4_topmetr :::"Closed-Interval-TSpace"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) "is" ($#v2_topalg_2 :::"interval"::: ) )) ; theorem :: TOPALG_2:10 (Bool (Set ($#k5_topmetr :::"I[01]"::: ) ) "is" ($#v2_topalg_2 :::"interval"::: ) ) ; theorem :: TOPALG_2:11 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "b")))) "holds" (Bool (Set ($#k4_topmetr :::"Closed-Interval-TSpace"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) "is" ($#v1_borsuk_2 :::"pathwise_connected"::: ) )) ; definitionlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_topalg_2 :::"interval"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set ($#k2_topalg_2 :::"R^1"::: ) ); let "P", "Q" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set (Const "T")); func :::"R1Homotopy"::: "(" "P" "," "Q" ")" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set ($#k5_topmetr :::"I[01]"::: ) ) ($#k2_borsuk_1 :::":]"::: ) ) "," "T" means :: TOPALG_2:def 4 (Bool "for" (Set (Var "s")) "," (Set (Var "t")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "holds" (Bool (Set it ($#k1_binop_1 :::"."::: ) "(" (Set (Var "s")) "," (Set (Var "t")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Num 1) ($#k9_real_1 :::"-"::: ) (Set (Var "t")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" "P" ($#k3_funct_2 :::"."::: ) (Set (Var "s")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "t")) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" "Q" ($#k3_funct_2 :::"."::: ) (Set (Var "s")) ")" ) ")" )))); end; :: deftheorem defines :::"R1Homotopy"::: TOPALG_2:def 4 : (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_topalg_2 :::"interval"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set ($#k2_topalg_2 :::"R^1"::: ) ) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set (Var "T")) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set ($#k5_topmetr :::"I[01]"::: ) ) ($#k2_borsuk_1 :::":]"::: ) ) "," (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k3_topalg_2 :::"R1Homotopy"::: ) "(" (Set (Var "P")) "," (Set (Var "Q")) ")" )) "iff" (Bool "for" (Set (Var "s")) "," (Set (Var "t")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "holds" (Bool (Set (Set (Var "b4")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "s")) "," (Set (Var "t")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Num 1) ($#k9_real_1 :::"-"::: ) (Set (Var "t")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "P")) ($#k3_funct_2 :::"."::: ) (Set (Var "s")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "t")) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "Q")) ($#k3_funct_2 :::"."::: ) (Set (Var "s")) ")" ) ")" )))) ")" )))); theorem :: TOPALG_2:12 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_topalg_2 :::"interval"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set ($#k2_topalg_2 :::"R^1"::: ) ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) "holds" (Bool (Set (Var "P")) "," (Set (Var "Q")) ($#r4_borsuk_2 :::"are_homotopic"::: ) )))) ; registrationlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_topalg_2 :::"interval"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set ($#k2_topalg_2 :::"R^1"::: ) ); let "a", "b" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "T")); let "P", "Q" be ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Const "a")) "," (Set (Const "b")); cluster -> ($#v5_pre_topc :::"continuous"::: ) for ($#m1_borsuk_6 :::"Homotopy"::: ) "of" "P" "," "Q"; end; theorem :: TOPALG_2:13 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_topalg_2 :::"interval"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set ($#k2_topalg_2 :::"R^1"::: ) ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "C")) "being" ($#m1_borsuk_2 :::"Loop":::) "of" (Set (Var "a")) "holds" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k5_topalg_1 :::"pi_1"::: ) "(" (Set (Var "T")) "," (Set (Var "a")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k4_topalg_1 :::"EqRel"::: ) "(" (Set (Var "T")) "," (Set (Var "a")) ")" ")" ) "," (Set (Var "C")) ")" ")" ) ($#k1_tarski :::"}"::: ) ))))) ; registrationlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_topalg_2 :::"interval"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set ($#k2_topalg_2 :::"R^1"::: ) ); let "a" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "T")); cluster (Set ($#k5_topalg_1 :::"FundamentalGroup"::: ) "(" "T" "," "a" ")" ) -> ($#v7_struct_0 :::"trivial"::: ) ; end; theorem :: TOPALG_2:14 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "b")))) "holds" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k4_topmetr :::"Closed-Interval-TSpace"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "x")) "," (Set (Var "y")) "holds" (Bool (Set (Var "P")) "," (Set (Var "Q")) ($#r3_borsuk_2 :::"are_homotopic"::: ) )))) ; theorem :: TOPALG_2:15 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "b")))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k4_topmetr :::"Closed-Interval-TSpace"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) (Bool "for" (Set (Var "C")) "being" ($#m1_borsuk_2 :::"Loop":::) "of" (Set (Var "x")) "holds" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k5_topalg_1 :::"pi_1"::: ) "(" (Set "(" ($#k4_topmetr :::"Closed-Interval-TSpace"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) "," (Set (Var "x")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k4_topalg_1 :::"EqRel"::: ) "(" (Set "(" ($#k4_topmetr :::"Closed-Interval-TSpace"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) "," (Set (Var "x")) ")" ")" ) "," (Set (Var "C")) ")" ")" ) ($#k1_tarski :::"}"::: ) ))))) ; theorem :: TOPALG_2:16 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "x")) "," (Set (Var "y")) "holds" (Bool (Set (Var "P")) "," (Set (Var "Q")) ($#r4_borsuk_2 :::"are_homotopic"::: ) ))) ; theorem :: TOPALG_2:17 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) (Bool "for" (Set (Var "C")) "being" ($#m1_borsuk_2 :::"Loop":::) "of" (Set (Var "x")) "holds" (Bool (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k5_topalg_1 :::"pi_1"::: ) "(" (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set (Var "x")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k4_topalg_1 :::"EqRel"::: ) "(" (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set (Var "x")) ")" ")" ) "," (Set (Var "C")) ")" ")" ) ($#k1_tarski :::"}"::: ) )))) ; registrationlet "x" be ($#m1_subset_1 :::"Point":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ); cluster (Set ($#k5_topalg_1 :::"FundamentalGroup"::: ) "(" (Set ($#k5_topmetr :::"I[01]"::: ) ) "," "x" ")" ) -> ($#v7_struct_0 :::"trivial"::: ) ; end; registrationlet "n" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ); let "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_topalg_2 :::"convex"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set ($#k15_euclid :::"TOP-REAL"::: ) (Set (Const "n"))); let "P", "Q" be ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set (Const "T")); cluster (Set ($#k1_topalg_2 :::"ConvexHomotopy"::: ) "(" "P" "," "Q" ")" ) -> ($#v5_pre_topc :::"continuous"::: ) ; end; theorem :: TOPALG_2:18 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_topalg_2 :::"convex"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n"))) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) "holds" (Bool (Set ($#k1_topalg_2 :::"ConvexHomotopy"::: ) "(" (Set (Var "P")) "," (Set (Var "Q")) ")" ) "is" ($#m1_borsuk_6 :::"Homotopy"::: ) "of" (Set (Var "P")) "," (Set (Var "Q"))))))) ; registrationlet "T" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_topalg_2 :::"interval"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set ($#k2_topalg_2 :::"R^1"::: ) ); let "P", "Q" be ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set (Const "T")); cluster (Set ($#k3_topalg_2 :::"R1Homotopy"::: ) "(" "P" "," "Q" ")" ) -> ($#v5_pre_topc :::"continuous"::: ) ; end; theorem :: TOPALG_2:19 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v2_topalg_2 :::"interval"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set ($#k2_topalg_2 :::"R^1"::: ) ) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "a")) "," (Set (Var "b")) "holds" (Bool (Set ($#k3_topalg_2 :::"R1Homotopy"::: ) "(" (Set (Var "P")) "," (Set (Var "Q")) ")" ) "is" ($#m1_borsuk_6 :::"Homotopy"::: ) "of" (Set (Var "P")) "," (Set (Var "Q")))))) ;