:: TOPALG_5 semantic presentation begin registration cluster (Set ($#k2_gr_cy_1 :::"INT.Group"::: ) ) -> ($#v8_struct_0 :::"infinite"::: ) ; end; theorem :: TOPALG_5:1 (Bool "for" (Set (Var "r")) "," (Set (Var "s")) "," (Set (Var "a")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "s")))) "holds" (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k2_topmetr :::"Closed-Interval-MSpace"::: ) "(" (Set (Var "r")) "," (Set (Var "s")) ")" ")" ) "holds" (Bool "(" (Bool (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "p")) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set (Var "r")) "," (Set (Var "s")) ($#k1_rcomp_1 :::".]"::: ) )) "or" (Bool (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "p")) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_rcomp_1 :::"[."::: ) (Set (Var "r")) "," (Set "(" (Set (Var "p")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "a")) ")" ) ($#k3_rcomp_1 :::".["::: ) )) "or" (Bool (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "p")) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_rcomp_1 :::"]."::: ) (Set "(" (Set (Var "p")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "a")) ")" ) "," (Set (Var "s")) ($#k4_rcomp_1 :::".]"::: ) )) "or" (Bool (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "p")) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" (Set (Var "p")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "a")) ")" ) "," (Set "(" (Set (Var "p")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "a")) ")" ) ($#k2_rcomp_1 :::".["::: ) )) ")" ))) ; theorem :: TOPALG_5:2 (Bool "for" (Set (Var "r")) "," (Set (Var "s")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "s")))) "holds" (Bool "ex" (Set (Var "B")) "being" ($#m1_subset_1 :::"Basis":::) "of" (Set "(" ($#k4_topmetr :::"Closed-Interval-TSpace"::: ) "(" (Set (Var "r")) "," (Set (Var "s")) ")" ")" ) "st" (Bool "(" (Bool "ex" (Set (Var "f")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set "(" ($#k4_topmetr :::"Closed-Interval-TSpace"::: ) "(" (Set (Var "r")) "," (Set (Var "s")) ")" ")" ) "st" (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k2_topmetr :::"Closed-Interval-MSpace"::: ) "(" (Set (Var "r")) "," (Set (Var "s")) ")" ")" ) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) "{" (Set "(" ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "y")) "," (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set (Var "n")) ")" ) ")" ")" ) where n "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool (Set (Var "n")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) "}" ) & (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set ($#k3_card_3 :::"Union"::: ) (Set (Var "f")))) ")" ))) & (Bool "(" "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k4_topmetr :::"Closed-Interval-TSpace"::: ) "(" (Set (Var "r")) "," (Set (Var "s")) ")" ")" ) "st" (Bool (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set (Var "B")))) "holds" (Bool (Set (Var "X")) "is" ($#v2_connsp_1 :::"connected"::: ) ) ")" ) ")" ))) ; theorem :: TOPALG_5:3 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopStruct"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set ($#k6_connsp_3 :::"Component_of"::: ) "(" (Set (Var "t")) "," (Set (Var "A")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Var "A")))))) ; registrationlet "T" be ($#l1_pre_topc :::"TopSpace":::); let "A" be ($#v3_pre_topc :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "T")); cluster (Set "T" ($#k1_pre_topc :::"|"::: ) "A") -> ($#v1_tsep_1 :::"open"::: ) ; end; theorem :: TOPALG_5:4 (Bool "for" (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "S")) "being" ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "T")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "B")))) "holds" (Bool (Set (Set (Var "T")) ($#k1_pre_topc :::"|"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "S")) ($#k1_pre_topc :::"|"::: ) (Set (Var "B")))))))) ; theorem :: TOPALG_5:5 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "S"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "T"))) "#)" )) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "C"))) & (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set (Var "D"))) & (Bool (Set (Var "A")) "," (Set (Var "B")) ($#r1_connsp_1 :::"are_separated"::: ) )) "holds" (Bool (Set (Var "C")) "," (Set (Var "D")) ($#r1_connsp_1 :::"are_separated"::: ) )))) ; theorem :: TOPALG_5:6 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) "st" (Bool (Bool (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "S"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "T"))) "#)" )) & (Bool (Set (Var "S")) "is" ($#v1_connsp_1 :::"connected"::: ) )) "holds" (Bool (Set (Var "T")) "is" ($#v1_connsp_1 :::"connected"::: ) )) ; theorem :: TOPALG_5:7 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "S"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "T"))) "#)" )) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "B"))) & (Bool (Set (Var "A")) "is" ($#v2_connsp_1 :::"connected"::: ) )) "holds" (Bool (Set (Var "B")) "is" ($#v2_connsp_1 :::"connected"::: ) )))) ; theorem :: TOPALG_5:8 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "A")) "being" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Var "s")) "st" (Bool (Bool (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "S"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "T"))) "#)" )) & (Bool (Set (Var "s")) ($#r1_hidden :::"="::: ) (Set (Var "t")))) "holds" (Bool (Set (Var "A")) "is" ($#m1_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Var "t"))))))) ; theorem :: TOPALG_5:9 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "N")) "being" ($#m2_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Var "A")) "st" (Bool (Bool (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "S"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "T"))) "#)" )) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "B")))) "holds" (Bool (Set (Var "N")) "is" ($#m2_connsp_2 :::"a_neighborhood"::: ) "of" (Set (Var "B"))))))) ; theorem :: TOPALG_5:10 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "T")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v3_tops_2 :::"being_homeomorphism"::: ) ) & (Bool (Set (Var "A")) ($#r3_connsp_1 :::"is_a_component_of"::: ) (Set (Var "B")))) "holds" (Bool (Set (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set (Var "A"))) ($#r3_connsp_1 :::"is_a_component_of"::: ) (Set (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set (Var "B"))))))) ; begin theorem :: TOPALG_5:11 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "T")) (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Var "B"))) & (Bool (Set (Var "A")) "is" ($#v2_connsp_2 :::"locally_connected"::: ) )) "holds" (Bool (Set (Var "B")) "is" ($#v2_connsp_2 :::"locally_connected"::: ) ))))) ; theorem :: TOPALG_5:12 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "st" (Bool (Bool (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "S"))) "#)" ) ($#r1_hidden :::"="::: ) (Set ($#g1_pre_topc :::"TopStruct"::: ) "(#" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "T"))) "," (Set "the" ($#u1_pre_topc :::"topology"::: ) "of" (Set (Var "T"))) "#)" )) & (Bool (Set (Var "S")) "is" ($#v1_connsp_2 :::"locally_connected"::: ) )) "holds" (Bool (Set (Var "T")) "is" ($#v1_connsp_2 :::"locally_connected"::: ) )) ; theorem :: TOPALG_5:13 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "holds" (Bool "(" (Bool (Set (Var "T")) "is" ($#v1_connsp_2 :::"locally_connected"::: ) ) "iff" (Bool (Set ($#k2_struct_0 :::"[#]"::: ) (Set (Var "T"))) "is" ($#v2_connsp_2 :::"locally_connected"::: ) ) ")" )) ; theorem :: TOPALG_5:14 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_tsep_1 :::"open"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "T")) "is" ($#v1_connsp_2 :::"locally_connected"::: ) )) "holds" (Bool (Set (Var "S")) "is" ($#v1_connsp_2 :::"locally_connected"::: ) ))) ; theorem :: TOPALG_5:15 (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "st" (Bool (Bool (Set (Var "S")) "," (Set (Var "T")) ($#r2_borsuk_3 :::"are_homeomorphic"::: ) ) & (Bool (Set (Var "S")) "is" ($#v1_connsp_2 :::"locally_connected"::: ) )) "holds" (Bool (Set (Var "T")) "is" ($#v1_connsp_2 :::"locally_connected"::: ) )) ; theorem :: TOPALG_5:16 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) "st" (Bool (Bool "ex" (Set (Var "B")) "being" ($#m1_subset_1 :::"Basis":::) "of" (Set (Var "T")) "st" (Bool "for" (Set (Var "X")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "X")) ($#r2_hidden :::"in"::: ) (Set (Var "B")))) "holds" (Bool (Set (Var "X")) "is" ($#v2_connsp_1 :::"connected"::: ) )))) "holds" (Bool (Set (Var "T")) "is" ($#v1_connsp_2 :::"locally_connected"::: ) )) ; theorem :: TOPALG_5:17 (Bool "for" (Set (Var "r")) "," (Set (Var "s")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "s")))) "holds" (Bool (Set ($#k4_topmetr :::"Closed-Interval-TSpace"::: ) "(" (Set (Var "r")) "," (Set (Var "s")) ")" ) "is" ($#v1_connsp_2 :::"locally_connected"::: ) )) ; registration cluster (Set ($#k17_borsuk_1 :::"I[01]"::: ) ) -> ($#v1_connsp_2 :::"locally_connected"::: ) ; end; registrationlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v3_pre_topc :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ); cluster (Set (Set ($#k5_topmetr :::"I[01]"::: ) ) ($#k1_pre_topc :::"|"::: ) "A") -> ($#v1_connsp_2 :::"locally_connected"::: ) ; end; begin definitionlet "r" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; func :::"ExtendInt"::: "r" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set ($#k2_topalg_2 :::"R^1"::: ) ) means :: TOPALG_5:def 1 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set "r" ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x"))))); end; :: deftheorem defines :::"ExtendInt"::: TOPALG_5:def 1 : (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set ($#k2_topalg_2 :::"R^1"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k1_topalg_5 :::"ExtendInt"::: ) (Set (Var "r")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "holds" (Bool (Set (Set (Var "b2")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "x"))))) ")" ))); registrationlet "r" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set ($#k1_topalg_5 :::"ExtendInt"::: ) "r") -> ($#v5_pre_topc :::"continuous"::: ) ; end; definitionlet "r" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; :: original: :::"ExtendInt"::: redefine func :::"ExtendInt"::: "r" -> ($#m1_borsuk_2 :::"Path"::: ) "of" (Set ($#k4_toprealb :::"R^1"::: ) (Set ($#k6_numbers :::"0"::: ) )) "," (Set ($#k4_toprealb :::"R^1"::: ) "r"); end; definitionlet "S", "T", "Y" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "H" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set (Const "S")) "," (Set (Const "T")) ($#k2_borsuk_1 :::":]"::: ) ) "," (Set (Const "Y")); let "t" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "T")); func :::"Prj1"::: "(" "t" "," "H" ")" -> ($#m1_subset_1 :::"Function":::) "of" "S" "," "Y" means :: TOPALG_5:def 2 (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Point":::) "of" "S" "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set "H" ($#k1_binop_1 :::"."::: ) "(" (Set (Var "s")) "," "t" ")" ))); end; :: deftheorem defines :::"Prj1"::: TOPALG_5:def 2 : (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "T")) ($#k2_borsuk_1 :::":]"::: ) ) "," (Set (Var "Y")) (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "b6")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Var "b6")) ($#r1_hidden :::"="::: ) (Set ($#k3_topalg_5 :::"Prj1"::: ) "(" (Set (Var "t")) "," (Set (Var "H")) ")" )) "iff" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set (Var "b6")) ($#k3_funct_2 :::"."::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "H")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "s")) "," (Set (Var "t")) ")" ))) ")" ))))); definitionlet "S", "T", "Y" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "H" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set (Const "S")) "," (Set (Const "T")) ($#k2_borsuk_1 :::":]"::: ) ) "," (Set (Const "Y")); let "s" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "S")); func :::"Prj2"::: "(" "s" "," "H" ")" -> ($#m1_subset_1 :::"Function":::) "of" "T" "," "Y" means :: TOPALG_5:def 3 (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"Point":::) "of" "T" "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set "H" ($#k1_binop_1 :::"."::: ) "(" "s" "," (Set (Var "t")) ")" ))); end; :: deftheorem defines :::"Prj2"::: TOPALG_5:def 3 : (Bool "for" (Set (Var "S")) "," (Set (Var "T")) "," (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "S")) "," (Set (Var "T")) ($#k2_borsuk_1 :::":]"::: ) ) "," (Set (Var "Y")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "b6")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Var "b6")) ($#r1_hidden :::"="::: ) (Set ($#k4_topalg_5 :::"Prj2"::: ) "(" (Set (Var "s")) "," (Set (Var "H")) ")" )) "iff" (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "T")) "holds" (Bool (Set (Set (Var "b6")) ($#k3_funct_2 :::"."::: ) (Set (Var "t"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "H")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "s")) "," (Set (Var "t")) ")" ))) ")" ))))); registrationlet "S", "T", "Y" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "H" be ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set (Const "S")) "," (Set (Const "T")) ($#k2_borsuk_1 :::":]"::: ) ) "," (Set (Const "Y")); let "t" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "T")); cluster (Set ($#k3_topalg_5 :::"Prj1"::: ) "(" "t" "," "H" ")" ) -> ($#v5_pre_topc :::"continuous"::: ) ; end; registrationlet "S", "T", "Y" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "H" be ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set (Const "S")) "," (Set (Const "T")) ($#k2_borsuk_1 :::":]"::: ) ) "," (Set (Const "Y")); let "s" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "S")); cluster (Set ($#k4_topalg_5 :::"Prj2"::: ) "(" "s" "," "H" ")" ) -> ($#v5_pre_topc :::"continuous"::: ) ; end; theorem :: TOPALG_5:18 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (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")) (Bool "for" (Set (Var "H")) "being" ($#m1_borsuk_6 :::"Homotopy"::: ) "of" (Set (Var "P")) "," (Set (Var "Q")) (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "st" (Bool (Bool (Set (Var "H")) "is" ($#v5_pre_topc :::"continuous"::: ) )) "holds" (Bool (Set ($#k3_topalg_5 :::"Prj1"::: ) "(" (Set (Var "t")) "," (Set (Var "H")) ")" ) "is" ($#v5_pre_topc :::"continuous"::: ) )))))) ; theorem :: TOPALG_5:19 (Bool "for" (Set (Var "T")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (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")) (Bool "for" (Set (Var "H")) "being" ($#m1_borsuk_6 :::"Homotopy"::: ) "of" (Set (Var "P")) "," (Set (Var "Q")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "st" (Bool (Bool (Set (Var "H")) "is" ($#v5_pre_topc :::"continuous"::: ) )) "holds" (Bool (Set ($#k4_topalg_5 :::"Prj2"::: ) "(" (Set (Var "s")) "," (Set (Var "H")) ")" ) "is" ($#v5_pre_topc :::"continuous"::: ) )))))) ; definitionlet "r" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; func :::"cLoop"::: "r" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set "(" ($#k8_toprealb :::"Tunit_circle"::: ) (Num 2) ")" ) means :: TOPALG_5:def 4 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k19_euclid :::"|["::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set "(" (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k8_real_1 :::"*"::: ) "r" ")" ) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) "," (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set "(" (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k8_real_1 :::"*"::: ) "r" ")" ) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) ($#k19_euclid :::"]|"::: ) ))); end; :: deftheorem defines :::"cLoop"::: TOPALG_5:def 4 : (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set "(" ($#k8_toprealb :::"Tunit_circle"::: ) (Num 2) ")" ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k5_topalg_5 :::"cLoop"::: ) (Set (Var "r")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "holds" (Bool (Set (Set (Var "b2")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k19_euclid :::"|["::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set "(" (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k8_real_1 :::"*"::: ) (Set (Var "r")) ")" ) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) "," (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set "(" (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k8_real_1 :::"*"::: ) (Set (Var "r")) ")" ) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) ($#k19_euclid :::"]|"::: ) ))) ")" ))); theorem :: TOPALG_5:20 (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k5_topalg_5 :::"cLoop"::: ) (Set (Var "r"))) ($#r2_funct_2 :::"="::: ) (Set (Set ($#k12_toprealb :::"CircleMap"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k2_topalg_5 :::"ExtendInt"::: ) (Set (Var "r")) ")" )))) ; definitionlet "n" be ($#m1_hidden :::"Integer":::); :: original: :::"cLoop"::: redefine func :::"cLoop"::: "n" -> ($#m1_borsuk_2 :::"Loop":::) "of" (Set ($#k9_toprealb :::"c[10]"::: ) ); end; begin theorem :: TOPALG_5:21 (Bool "for" (Set (Var "UL")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set "(" ($#k8_toprealb :::"Tunit_circle"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "UL")) "is" ($#m1_setfam_1 :::"Cover":::) "of" (Set "(" ($#k8_toprealb :::"Tunit_circle"::: ) (Num 2) ")" )) & (Bool (Set (Var "UL")) "is" ($#v1_tops_2 :::"open"::: ) )) "holds" (Bool "for" (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "F")) "being" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "Y")) "," (Set ($#k5_topmetr :::"I[01]"::: ) ) ($#k2_borsuk_1 :::":]"::: ) ) "," (Set "(" ($#k8_toprealb :::"Tunit_circle"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "Y")) (Bool "ex" (Set (Var "T")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool "(" (Bool (Set (Set (Var "T")) ($#k1_seq_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set (Var "T")) ($#k1_seq_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "T")) ")" )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Var "T")) "is" ($#v5_valued_0 :::"increasing"::: ) ) & (Bool "ex" (Set (Var "N")) "being" ($#v3_pre_topc :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "Y")) "st" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "N"))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "T")))) & (Bool (Set (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1)) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "T"))))) "holds" (Bool "ex" (Set (Var "Ui")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k8_toprealb :::"Tunit_circle"::: ) (Num 2) ")" ) "st" (Bool "(" (Bool (Set (Var "Ui")) ($#r2_hidden :::"in"::: ) (Set (Var "UL"))) & (Bool (Set (Set (Var "F")) ($#k7_relset_1 :::".:"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "N")) "," (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" (Set (Var "T")) ($#k1_seq_1 :::"."::: ) (Set (Var "i")) ")" ) "," (Set "(" (Set (Var "T")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set (Var "i")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ($#k1_rcomp_1 :::".]"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )) ($#r1_tarski :::"c="::: ) (Set (Var "Ui"))) ")" )) ")" ) ")" )) ")" )))))) ; theorem :: TOPALG_5:22 (Bool "for" (Set (Var "Y")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "Y")) "," (Set ($#k5_topmetr :::"I[01]"::: ) ) ($#k2_borsuk_1 :::":]"::: ) ) "," (Set "(" ($#k8_toprealb :::"Tunit_circle"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "Ft")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "Y")) "," (Set "(" ($#k1_tex_2 :::"Sspace"::: ) (Set ($#k18_borsuk_1 :::"0[01]"::: ) ) ")" ) ($#k2_borsuk_1 :::":]"::: ) ) "," (Set ($#k2_topalg_2 :::"R^1"::: ) ) "st" (Bool (Bool (Set (Var "F")) "is" ($#v5_pre_topc :::"continuous"::: ) ) & (Bool (Set (Var "Ft")) "is" ($#v5_pre_topc :::"continuous"::: ) ) & (Bool (Set (Set (Var "F")) ($#k2_partfun1 :::"|"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y"))) "," (Set ($#k6_domain_1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k6_domain_1 :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set ($#k12_toprealb :::"CircleMap"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set (Var "Ft"))))) "holds" (Bool "ex" (Set (Var "G")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "Y")) "," (Set ($#k5_topmetr :::"I[01]"::: ) ) ($#k2_borsuk_1 :::":]"::: ) ) "," (Set ($#k2_topalg_2 :::"R^1"::: ) ) "st" (Bool "(" (Bool (Set (Var "G")) "is" ($#v5_pre_topc :::"continuous"::: ) ) & (Bool (Set (Var "F")) ($#r2_funct_2 :::"="::: ) (Set (Set ($#k12_toprealb :::"CircleMap"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set (Var "G")))) & (Bool (Set (Set (Var "G")) ($#k2_partfun1 :::"|"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y"))) "," (Set ($#k6_domain_1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k6_domain_1 :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "Ft"))) & (Bool "(" "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_borsuk_1 :::"[:"::: ) (Set (Var "Y")) "," (Set ($#k5_topmetr :::"I[01]"::: ) ) ($#k2_borsuk_1 :::":]"::: ) ) "," (Set ($#k2_topalg_2 :::"R^1"::: ) ) "st" (Bool (Bool (Set (Var "H")) "is" ($#v5_pre_topc :::"continuous"::: ) ) & (Bool (Set (Var "F")) ($#r2_funct_2 :::"="::: ) (Set (Set ($#k12_toprealb :::"CircleMap"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set (Var "H")))) & (Bool (Set (Set (Var "H")) ($#k2_partfun1 :::"|"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "Y"))) "," (Set ($#k6_domain_1 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k6_domain_1 :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "Ft")))) "holds" (Bool (Set (Var "G")) ($#r2_funct_2 :::"="::: ) (Set (Var "H"))) ")" ) ")" ))))) ; theorem :: TOPALG_5:23 (Bool "for" (Set (Var "x0")) "," (Set (Var "y0")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k8_toprealb :::"Tunit_circle"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "xt")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k2_topalg_2 :::"R^1"::: ) ) (Bool "for" (Set (Var "f")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "x0")) "," (Set (Var "y0")) "st" (Bool (Bool (Set (Var "xt")) ($#r2_hidden :::"in"::: ) (Set (Set ($#k12_toprealb :::"CircleMap"::: ) ) ($#k8_relset_1 :::"""::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x0")) ($#k6_domain_1 :::"}"::: ) )))) "holds" (Bool "ex" (Set (Var "ft")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set ($#k2_topalg_2 :::"R^1"::: ) ) "st" (Bool "(" (Bool (Set (Set (Var "ft")) ($#k1_seq_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "xt"))) & (Bool (Set (Var "f")) ($#r2_funct_2 :::"="::: ) (Set (Set ($#k12_toprealb :::"CircleMap"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set (Var "ft")))) & (Bool (Set (Var "ft")) "is" ($#v5_pre_topc :::"continuous"::: ) ) & (Bool "(" "for" (Set (Var "f1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k5_topmetr :::"I[01]"::: ) ) "," (Set ($#k2_topalg_2 :::"R^1"::: ) ) "st" (Bool (Bool (Set (Var "f1")) "is" ($#v5_pre_topc :::"continuous"::: ) ) & (Bool (Set (Var "f")) ($#r2_funct_2 :::"="::: ) (Set (Set ($#k12_toprealb :::"CircleMap"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set (Var "f1")))) & (Bool (Set (Set (Var "f1")) ($#k1_seq_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "xt")))) "holds" (Bool (Set (Var "ft")) ($#r2_funct_2 :::"="::: ) (Set (Var "f1"))) ")" ) ")" ))))) ; theorem :: TOPALG_5:24 (Bool "for" (Set (Var "x0")) "," (Set (Var "y0")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k8_toprealb :::"Tunit_circle"::: ) (Num 2) ")" ) (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "x0")) "," (Set (Var "y0")) (Bool "for" (Set (Var "F")) "being" ($#m1_borsuk_6 :::"Homotopy"::: ) "of" (Set (Var "P")) "," (Set (Var "Q")) (Bool "for" (Set (Var "xt")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k2_topalg_2 :::"R^1"::: ) ) "st" (Bool (Bool (Set (Var "P")) "," (Set (Var "Q")) ($#r4_borsuk_2 :::"are_homotopic"::: ) ) & (Bool (Set (Var "xt")) ($#r2_hidden :::"in"::: ) (Set (Set ($#k12_toprealb :::"CircleMap"::: ) ) ($#k8_relset_1 :::"""::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "x0")) ($#k6_domain_1 :::"}"::: ) )))) "holds" (Bool "ex" (Set (Var "yt")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k2_topalg_2 :::"R^1"::: ) )(Bool "ex" (Set (Var "Pt")) "," (Set (Var "Qt")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Var "xt")) "," (Set (Var "yt"))(Bool "ex" (Set (Var "Ft")) "being" ($#m1_borsuk_6 :::"Homotopy"::: ) "of" (Set (Var "Pt")) "," (Set (Var "Qt")) "st" (Bool "(" (Bool (Set (Var "Pt")) "," (Set (Var "Qt")) ($#r4_borsuk_2 :::"are_homotopic"::: ) ) & (Bool (Set (Var "F")) ($#r2_funct_2 :::"="::: ) (Set (Set ($#k12_toprealb :::"CircleMap"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set (Var "Ft")))) & (Bool (Set (Var "yt")) ($#r2_hidden :::"in"::: ) (Set (Set ($#k12_toprealb :::"CircleMap"::: ) ) ($#k8_relset_1 :::"""::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set (Var "y0")) ($#k6_domain_1 :::"}"::: ) ))) & (Bool "(" "for" (Set (Var "F1")) "being" ($#m1_borsuk_6 :::"Homotopy"::: ) "of" (Set (Var "Pt")) "," (Set (Var "Qt")) "st" (Bool (Bool (Set (Var "F")) ($#r2_funct_2 :::"="::: ) (Set (Set ($#k12_toprealb :::"CircleMap"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set (Var "F1"))))) "holds" (Bool (Set (Var "Ft")) ($#r2_funct_2 :::"="::: ) (Set (Var "F1"))) ")" ) ")" )))))))) ; definitionfunc :::"Ciso"::: -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_gr_cy_1 :::"INT.Group"::: ) ) "," (Set "(" ($#k5_topalg_1 :::"pi_1"::: ) "(" (Set "(" ($#k8_toprealb :::"Tunit_circle"::: ) (Num 2) ")" ) "," (Set ($#k9_toprealb :::"c[10]"::: ) ) ")" ")" ) means :: TOPALG_5:def 5 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k4_topalg_1 :::"EqRel"::: ) "(" (Set "(" ($#k8_toprealb :::"Tunit_circle"::: ) (Num 2) ")" ) "," (Set ($#k9_toprealb :::"c[10]"::: ) ) ")" ")" ) "," (Set "(" ($#k6_topalg_5 :::"cLoop"::: ) (Set (Var "n")) ")" ) ")" ))); end; :: deftheorem defines :::"Ciso"::: TOPALG_5:def 5 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_gr_cy_1 :::"INT.Group"::: ) ) "," (Set "(" ($#k5_topalg_1 :::"pi_1"::: ) "(" (Set "(" ($#k8_toprealb :::"Tunit_circle"::: ) (Num 2) ")" ) "," (Set ($#k9_toprealb :::"c[10]"::: ) ) ")" ")" ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k7_topalg_5 :::"Ciso"::: ) )) "iff" (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool (Set (Set (Var "b1")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k4_topalg_1 :::"EqRel"::: ) "(" (Set "(" ($#k8_toprealb :::"Tunit_circle"::: ) (Num 2) ")" ) "," (Set ($#k9_toprealb :::"c[10]"::: ) ) ")" ")" ) "," (Set "(" ($#k6_topalg_5 :::"cLoop"::: ) (Set (Var "n")) ")" ) ")" ))) ")" )); theorem :: TOPALG_5:25 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "f")) "being" ($#m1_borsuk_2 :::"Path"::: ) "of" (Set ($#k4_toprealb :::"R^1"::: ) (Set ($#k6_numbers :::"0"::: ) )) "," (Set ($#k4_toprealb :::"R^1"::: ) (Set (Var "i"))) "holds" (Bool (Set (Set ($#k7_topalg_5 :::"Ciso"::: ) ) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k6_eqrel_1 :::"Class"::: ) "(" (Set "(" ($#k4_topalg_1 :::"EqRel"::: ) "(" (Set "(" ($#k8_toprealb :::"Tunit_circle"::: ) (Num 2) ")" ) "," (Set ($#k9_toprealb :::"c[10]"::: ) ) ")" ")" ) "," (Set "(" (Set ($#k12_toprealb :::"CircleMap"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" ) ")" )))) ; registration cluster (Set ($#k7_topalg_5 :::"Ciso"::: ) ) -> ($#v1_group_6 :::"multiplicative"::: ) ; end; registration cluster (Set ($#k7_topalg_5 :::"Ciso"::: ) ) -> ($#v2_funct_1 :::"one-to-one"::: ) ($#v2_funct_2 :::"onto"::: ) ; end; theorem :: TOPALG_5:26 (Bool (Set ($#k7_topalg_5 :::"Ciso"::: ) ) "is" ($#v3_funct_2 :::"bijective"::: ) ) ; theorem :: TOPALG_5:27 (Bool "for" (Set (Var "S")) "being" ($#v1_toprealb :::"being_simple_closed_curve"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set ($#k15_euclid :::"TOP-REAL"::: ) (Num 2)) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k2_gr_cy_1 :::"INT.Group"::: ) ) "," (Set ($#k5_topalg_1 :::"pi_1"::: ) "(" (Set (Var "S")) "," (Set (Var "x")) ")" ) ($#r2_group_6 :::"are_isomorphic"::: ) ))) ; registrationlet "S" be ($#v1_toprealb :::"being_simple_closed_curve"::: ) ($#m1_pre_topc :::"SubSpace"::: ) "of" (Set ($#k15_euclid :::"TOP-REAL"::: ) (Num 2)); let "x" be ($#m1_subset_1 :::"Point":::) "of" (Set (Const "S")); cluster (Set ($#k5_topalg_1 :::"FundamentalGroup"::: ) "(" "S" "," "x" ")" ) -> ($#v8_struct_0 :::"infinite"::: ) ; end;