:: BORSUK_7 semantic presentation begin registration cluster -> ($#v1_rat_1 :::"irrational"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_borsuk_5 :::"IRRAT"::: ) ); end; theorem :: BORSUK_7:1 (Bool "for" (Set (Var "r")) "," (Set (Var "s")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "s"))) & (Bool (Set (Set (Var "r")) ($#k3_square_1 :::"^2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k3_square_1 :::"^2"::: ) ))) "holds" (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Set (Var "s")))) ; theorem :: BORSUK_7:2 (Bool "for" (Set (Var "r")) "," (Set (Var "s")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k4_int_1 :::"frac"::: ) (Set (Var "r"))) ($#r1_xxreal_0 :::">="::: ) (Set ($#k4_int_1 :::"frac"::: ) (Set (Var "s"))))) "holds" (Bool (Set ($#k4_int_1 :::"frac"::: ) (Set "(" (Set (Var "r")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "s")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_int_1 :::"frac"::: ) (Set (Var "r")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k4_int_1 :::"frac"::: ) (Set (Var "s")) ")" )))) ; theorem :: BORSUK_7:3 (Bool "for" (Set (Var "r")) "," (Set (Var "s")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k4_int_1 :::"frac"::: ) (Set (Var "r"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k4_int_1 :::"frac"::: ) (Set (Var "s"))))) "holds" (Bool (Set ($#k4_int_1 :::"frac"::: ) (Set "(" (Set (Var "r")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "s")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k4_int_1 :::"frac"::: ) (Set (Var "r")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k4_int_1 :::"frac"::: ) (Set (Var "s")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Num 1)))) ; theorem :: BORSUK_7:4 (Bool "for" (Set (Var "r")) "," (Set (Var "s")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "ex" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool "(" (Bool (Set ($#k4_int_1 :::"frac"::: ) (Set "(" (Set (Var "r")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "s")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k4_int_1 :::"frac"::: ) (Set (Var "r")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k4_int_1 :::"frac"::: ) (Set (Var "s")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set (Var "i")))) & (Bool "(" (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "or" (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Num 1)) ")" ) ")" ))) ; theorem :: BORSUK_7:5 (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" "not" (Bool (Set ($#k17_sin_cos :::"sin"::: ) (Set (Var "r"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "or" (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k8_real_1 :::"*"::: ) (Set ($#k1_int_1 :::"[\"::: ) (Set "(" (Set (Var "r")) ($#k13_complex1 :::"/"::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ")" ) ($#k1_int_1 :::"/]"::: ) ))) "or" (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Set (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k8_real_1 :::"*"::: ) (Set ($#k1_int_1 :::"[\"::: ) (Set "(" (Set (Var "r")) ($#k13_complex1 :::"/"::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ")" ) ($#k1_int_1 :::"/]"::: ) ) ")" ))) ")" )) ; theorem :: BORSUK_7:6 (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" "not" (Bool (Set ($#k20_sin_cos :::"cos"::: ) (Set (Var "r"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) "or" (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k13_complex1 :::"/"::: ) (Num 2) ")" ) ($#k3_real_1 :::"+"::: ) (Set "(" (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k8_real_1 :::"*"::: ) (Set ($#k1_int_1 :::"[\"::: ) (Set "(" (Set (Var "r")) ($#k13_complex1 :::"/"::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ")" ) ($#k1_int_1 :::"/]"::: ) ) ")" ))) "or" (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Num 3) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k13_complex1 :::"/"::: ) (Num 2) ")" ) ($#k3_real_1 :::"+"::: ) (Set "(" (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k8_real_1 :::"*"::: ) (Set ($#k1_int_1 :::"[\"::: ) (Set "(" (Set (Var "r")) ($#k13_complex1 :::"/"::: ) (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ")" ) ($#k1_int_1 :::"/]"::: ) ) ")" ))) ")" )) ; theorem :: BORSUK_7:7 (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k17_sin_cos :::"sin"::: ) (Set (Var "r"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "ex" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Set (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k8_real_1 :::"*"::: ) (Set (Var "i")))))) ; theorem :: BORSUK_7:8 (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k20_sin_cos :::"cos"::: ) (Set (Var "r"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "ex" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k13_complex1 :::"/"::: ) (Num 2) ")" ) ($#k3_real_1 :::"+"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k8_real_1 :::"*"::: ) (Set (Var "i")) ")" ))))) ; theorem :: BORSUK_7:9 (Bool "for" (Set (Var "r")) "," (Set (Var "s")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k17_sin_cos :::"sin"::: ) (Set (Var "r"))) ($#r1_hidden :::"="::: ) (Set ($#k17_sin_cos :::"sin"::: ) (Set (Var "s"))))) "holds" (Bool "ex" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool "(" (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k3_real_1 :::"+"::: ) (Set "(" (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k8_real_1 :::"*"::: ) (Set (Var "i")) ")" ))) "or" (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k9_real_1 :::"-"::: ) (Set (Var "s")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k8_real_1 :::"*"::: ) (Set (Var "i")) ")" ))) ")" ))) ; theorem :: BORSUK_7:10 (Bool "for" (Set (Var "r")) "," (Set (Var "s")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k20_sin_cos :::"cos"::: ) (Set (Var "r"))) ($#r1_hidden :::"="::: ) (Set ($#k20_sin_cos :::"cos"::: ) (Set (Var "s"))))) "holds" (Bool "ex" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool "(" (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k3_real_1 :::"+"::: ) (Set "(" (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k8_real_1 :::"*"::: ) (Set (Var "i")) ")" ))) "or" (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "s")) ")" ) ($#k3_real_1 :::"+"::: ) (Set "(" (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k8_real_1 :::"*"::: ) (Set (Var "i")) ")" ))) ")" ))) ; theorem :: BORSUK_7:11 (Bool "for" (Set (Var "r")) "," (Set (Var "s")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k17_sin_cos :::"sin"::: ) (Set (Var "r"))) ($#r1_hidden :::"="::: ) (Set ($#k17_sin_cos :::"sin"::: ) (Set (Var "s")))) & (Bool (Set ($#k20_sin_cos :::"cos"::: ) (Set (Var "r"))) ($#r1_hidden :::"="::: ) (Set ($#k20_sin_cos :::"cos"::: ) (Set (Var "s"))))) "holds" (Bool "ex" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k3_real_1 :::"+"::: ) (Set "(" (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k8_real_1 :::"*"::: ) (Set (Var "i")) ")" ))))) ; theorem :: BORSUK_7:12 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "c1")) "," (Set (Var "c2")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k17_complex1 :::"|."::: ) (Set (Var "c1")) ($#k17_complex1 :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k17_complex1 :::"|."::: ) (Set (Var "c2")) ($#k17_complex1 :::".|"::: ) )) & (Bool (Set ($#k1_comptrig :::"Arg"::: ) (Set (Var "c1"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_comptrig :::"Arg"::: ) (Set (Var "c2")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k8_real_1 :::"*"::: ) (Set (Var "i")) ")" )))) "holds" (Bool (Set (Var "c1")) ($#r1_hidden :::"="::: ) (Set (Var "c2"))))) ; registrationlet "f" be ($#v2_funct_1 :::"one-to-one"::: ) ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::); let "c" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "c" ($#k7_valued_1 :::"+"::: ) "f") -> ($#v2_funct_1 :::"one-to-one"::: ) ; end; registrationlet "f" be ($#v2_funct_1 :::"one-to-one"::: ) ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::); let "c" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "f" ($#k13_valued_1 :::"-"::: ) "c") -> ($#v2_funct_1 :::"one-to-one"::: ) ; end; theorem :: BORSUK_7:13 (Bool "for" (Set (Var "f")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k30_valued_1 :::"-"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))))) ; theorem :: BORSUK_7:14 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k6_euclid :::"-"::: ) (Set "(" ($#k5_euclid :::"0*"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_euclid :::"0*"::: ) (Set (Var "n"))))) ; theorem :: BORSUK_7:15 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "f")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"<>"::: ) (Set ($#k5_euclid :::"0*"::: ) (Set (Var "n"))))) "holds" (Bool (Set ($#k30_valued_1 :::"-"::: ) (Set (Var "f"))) ($#r1_hidden :::"<>"::: ) (Set ($#k5_euclid :::"0*"::: ) (Set (Var "n")))))) ; theorem :: BORSUK_7:16 (Bool "for" (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "r3")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k12_rvsum_1 :::"sqr"::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "r3")) ($#k11_finseq_1 :::"*>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "r1")) ($#k3_square_1 :::"^2"::: ) ")" ) "," (Set "(" (Set (Var "r2")) ($#k3_square_1 :::"^2"::: ) ")" ) "," (Set "(" (Set (Var "r3")) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k11_finseq_1 :::"*>"::: ) ))) ; theorem :: BORSUK_7:17 (Bool "for" (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "r3")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set "(" ($#k12_rvsum_1 :::"sqr"::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "r1")) "," (Set (Var "r2")) "," (Set (Var "r3")) ($#k11_finseq_1 :::"*>"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "r1")) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "r2")) ($#k3_square_1 :::"^2"::: ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "r3")) ($#k3_square_1 :::"^2"::: ) ")" )))) ; theorem :: BORSUK_7:18 (Bool "for" (Set (Var "c")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "f")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set (Set "(" (Set (Var "c")) ($#k24_valued_1 :::"(#)"::: ) (Set (Var "f")) ")" ) ($#k39_valued_1 :::"^2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "c")) ($#k3_square_1 :::"^2"::: ) ")" ) ($#k24_valued_1 :::"(#)"::: ) (Set "(" (Set (Var "f")) ($#k39_valued_1 :::"^2"::: ) ")" ))))) ; theorem :: BORSUK_7:19 (Bool "for" (Set (Var "c")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "f")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k14_valued_2 :::"(/)"::: ) (Set (Var "c")) ")" ) ($#k39_valued_1 :::"^2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k39_valued_1 :::"^2"::: ) ")" ) ($#k14_valued_2 :::"(/)"::: ) (Set "(" (Set (Var "c")) ($#k3_square_1 :::"^2"::: ) ")" ))))) ; theorem :: BORSUK_7:20 (Bool "for" (Set (Var "f")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set ($#k16_rvsum_1 :::"Sum"::: ) (Set (Var "f"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k16_rvsum_1 :::"Sum"::: ) (Set "(" (Set (Var "f")) ($#k14_valued_2 :::"(/)"::: ) (Set "(" ($#k16_rvsum_1 :::"Sum"::: ) (Set (Var "f")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Num 1))) ; definitionlet "a", "b", "c", "x", "y", "z" be ($#m1_hidden :::"set"::: ) ; func "(" "a" "," "b" "," "c" ")" :::"-->"::: "(" "x" "," "y" "," "z" ")" -> ($#m1_hidden :::"set"::: ) equals :: BORSUK_7:def 1 (Set (Set "(" "(" "a" "," "b" ")" ($#k4_funct_4 :::"-->"::: ) "(" "x" "," "y" ")" ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" "c" ($#k16_funcop_1 :::".-->"::: ) "z" ")" )); end; :: deftheorem defines :::"-->"::: BORSUK_7:def 1 : (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ($#k1_borsuk_7 :::"-->"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" "(" (Set (Var "a")) "," (Set (Var "b")) ")" ($#k4_funct_4 :::"-->"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "c")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "z")) ")" )))); registrationlet "a", "b", "c", "x", "y", "z" be ($#m1_hidden :::"set"::: ) ; cluster (Set "(" "a" "," "b" "," "c" ")" ($#k1_borsuk_7 :::"-->"::: ) "(" "x" "," "y" "," "z" ")" ) -> ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ; end; theorem :: BORSUK_7:21 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "c")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ($#k1_borsuk_7 :::"-->"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_enumset1 :::"{"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ($#k1_enumset1 :::"}"::: ) )))) ; theorem :: BORSUK_7:22 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "c")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ($#k1_borsuk_7 :::"-->"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ")" ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k1_enumset1 :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k1_enumset1 :::"}"::: ) )))) ; theorem :: BORSUK_7:23 (Bool "for" (Set (Var "a")) "," (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set "(" (Set (Var "a")) "," (Set (Var "a")) "," (Set (Var "a")) ")" ($#k1_borsuk_7 :::"-->"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "z"))))) ; theorem :: BORSUK_7:24 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set "(" (Set (Var "a")) "," (Set (Var "a")) "," (Set (Var "b")) ")" ($#k1_borsuk_7 :::"-->"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ")" ) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "a")) "," (Set (Var "b")) ")" ($#k4_funct_4 :::"-->"::: ) "(" (Set (Var "y")) "," (Set (Var "z")) ")" ))) ; theorem :: BORSUK_7:25 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b")))) "holds" (Bool (Set "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "a")) ")" ($#k1_borsuk_7 :::"-->"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ")" ) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "a")) "," (Set (Var "b")) ")" ($#k4_funct_4 :::"-->"::: ) "(" (Set (Var "z")) "," (Set (Var "y")) ")" ))) ; theorem :: BORSUK_7:26 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "b")) ")" ($#k1_borsuk_7 :::"-->"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ")" ) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "a")) "," (Set (Var "b")) ")" ($#k4_funct_4 :::"-->"::: ) "(" (Set (Var "x")) "," (Set (Var "z")) ")" ))) ; theorem :: BORSUK_7:27 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "c")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "c")))) "holds" (Bool (Set (Set "(" "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ($#k1_borsuk_7 :::"-->"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "x"))))) ; theorem :: BORSUK_7:28 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "c")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ($#r1_zfmisc_1 :::"are_mutually_different"::: ) )) "holds" (Bool "(" (Bool (Set (Set "(" "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ($#k1_borsuk_7 :::"-->"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set (Set "(" "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ($#k1_borsuk_7 :::"-->"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Var "y"))) & (Bool (Set (Set "(" "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ($#k1_borsuk_7 :::"-->"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Var "z"))) ")" ))) ; theorem :: BORSUK_7:29 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "c")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k1_enumset1 :::"{"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ($#k1_enumset1 :::"}"::: ) )) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Var "y"))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Var "z")))) "holds" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ($#k1_borsuk_7 :::"-->"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ")" ))))) ; theorem :: BORSUK_7:30 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "c")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k11_finseq_1 :::"<*"::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ($#k11_finseq_1 :::"*>"::: ) ) ($#r1_hidden :::"="::: ) (Set "(" (Num 1) "," (Num 2) "," (Num 3) ")" ($#k1_borsuk_7 :::"-->"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" )))) ; theorem :: BORSUK_7:31 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "c")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ($#r1_zfmisc_1 :::"are_mutually_different"::: ) )) "holds" (Bool (Set ($#k4_card_3 :::"product"::: ) (Set "(" "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ($#k1_borsuk_7 :::"-->"::: ) "(" (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) ) "," (Set ($#k1_tarski :::"{"::: ) (Set (Var "z")) ($#k1_tarski :::"}"::: ) ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ($#k1_borsuk_7 :::"-->"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ")" ")" ) ($#k1_tarski :::"}"::: ) )))) ; theorem :: BORSUK_7:32 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "c")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "F")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B"))) & (Bool (Set (Var "C")) ($#r1_tarski :::"c="::: ) (Set (Var "D"))) & (Bool (Set (Var "E")) ($#r1_tarski :::"c="::: ) (Set (Var "F")))) "holds" (Bool (Set ($#k4_card_3 :::"product"::: ) (Set "(" "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ($#k1_borsuk_7 :::"-->"::: ) "(" (Set (Var "A")) "," (Set (Var "C")) "," (Set (Var "E")) ")" ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k4_card_3 :::"product"::: ) (Set "(" "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ($#k1_borsuk_7 :::"-->"::: ) "(" (Set (Var "B")) "," (Set (Var "D")) "," (Set (Var "F")) ")" ")" )))))) ; theorem :: BORSUK_7:33 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "x")) "," (Set (Var "X")) "," (Set (Var "y")) "," (Set (Var "Y")) "," (Set (Var "z")) "," (Set (Var "Z")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "c")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ($#r1_zfmisc_1 :::"are_mutually_different"::: ) ) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "Y"))) & (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ($#k1_borsuk_7 :::"-->"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k4_card_3 :::"product"::: ) (Set "(" "(" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ")" ($#k1_borsuk_7 :::"-->"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) ")" ")" ))))) ; definitionlet "f" be ($#m1_hidden :::"Function":::); attr "f" is :::"odd"::: means :: BORSUK_7:def 2 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "f")) & (Bool (Set ($#k30_valued_1 :::"-"::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "f")) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set "f" ($#k1_funct_1 :::"."::: ) (Set (Var "x"))))) "holds" (Bool (Set "f" ($#k1_funct_1 :::"."::: ) (Set "(" ($#k30_valued_1 :::"-"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k30_valued_1 :::"-"::: ) (Set (Var "y"))))); end; :: deftheorem defines :::"odd"::: BORSUK_7:def 2 : (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v1_borsuk_7 :::"odd"::: ) ) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set ($#k30_valued_1 :::"-"::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k30_valued_1 :::"-"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k30_valued_1 :::"-"::: ) (Set (Var "y"))))) ")" )); registration cluster (Set ($#k1_xboole_0 :::"{}"::: ) ) -> ($#v1_borsuk_7 :::"odd"::: ) ; end; registration cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v7_valued_2 :::"complex-functions-valued"::: ) ($#v1_borsuk_7 :::"odd"::: ) for ($#m1_hidden :::"set"::: ) ; end; theorem :: BORSUK_7:34 (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 3) ")" ) "holds" (Bool (Set ($#k12_toprealc :::"sqr"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k11_finseq_1 :::"<*"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k1_euclid_5 :::"`1"::: ) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) "," (Set "(" (Set "(" (Set (Var "p")) ($#k2_euclid_5 :::"`2"::: ) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) "," (Set "(" (Set "(" (Set (Var "p")) ($#k3_euclid_5 :::"`3"::: ) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k11_finseq_1 :::"*>"::: ) ))) ; theorem :: BORSUK_7:35 (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 3) ")" ) "holds" (Bool (Set ($#k16_rvsum_1 :::"Sum"::: ) (Set "(" ($#k12_toprealc :::"sqr"::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set "(" (Set (Var "p")) ($#k1_euclid_5 :::"`1"::: ) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k2_euclid_5 :::"`2"::: ) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k3_euclid_5 :::"`3"::: ) ")" ) ($#k5_square_1 :::"^2"::: ) ")" )))) ; theorem :: BORSUK_7:36 (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_topmetr :::"R^1"::: ) ) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set ($#k3_numbers :::"RAT"::: ) ))) "holds" (Bool (Set (Set ($#k3_numbers :::"RAT"::: ) ) ($#k9_subset_1 :::"/\"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set ($#k2_xxreal_0 :::"-infty"::: ) ) "," (Set (Var "r")) ($#k2_rcomp_1 :::".["::: ) )) "is" ($#v3_pre_topc :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set ($#k3_topmetr :::"R^1"::: ) ) ($#k1_pre_topc :::"|"::: ) (Set (Var "S")) ")" )))) ; theorem :: BORSUK_7:37 (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_topmetr :::"R^1"::: ) ) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set ($#k3_numbers :::"RAT"::: ) ))) "holds" (Bool (Set (Set ($#k3_numbers :::"RAT"::: ) ) ($#k9_subset_1 :::"/\"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set (Var "r")) "," (Set ($#k1_xxreal_0 :::"+infty"::: ) ) ($#k2_rcomp_1 :::".["::: ) )) "is" ($#v3_pre_topc :::"open"::: ) ($#m1_subset_1 :::"Subset":::) "of" (Set "(" (Set ($#k3_topmetr :::"R^1"::: ) ) ($#k1_pre_topc :::"|"::: ) (Set (Var "S")) ")" )))) ; registrationlet "X" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#v1_connsp_1 :::"connected"::: ) ($#l1_pre_topc :::"TopSpace":::); let "Y" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_pre_topc :::"TopSpace":::); let "f" be ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Const "X")) "," (Set (Const "Y")); cluster (Set ($#k7_waybel18 :::"Image"::: ) "f") -> ($#v1_connsp_1 :::"connected"::: ) ; end; theorem :: BORSUK_7:38 (Bool "for" (Set (Var "S")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k3_topmetr :::"R^1"::: ) ) "st" (Bool (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set ($#k3_numbers :::"RAT"::: ) ))) "holds" (Bool "for" (Set (Var "T")) "being" ($#v1_connsp_1 :::"connected"::: ) ($#l1_pre_topc :::"TopSpace":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "T")) "," (Set "(" (Set ($#k3_topmetr :::"R^1"::: ) ) ($#k1_pre_topc :::"|"::: ) (Set (Var "S")) ")" ) "st" (Bool (Bool (Set (Var "f")) "is" ($#v5_pre_topc :::"continuous"::: ) )) "holds" (Bool (Set (Var "f")) "is" ($#v3_funct_1 :::"constant"::: ) )))) ; theorem :: BORSUK_7:39 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "f")) "being" ($#v5_pre_topc :::"continuous"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k4_topmetr :::"Closed-Interval-TSpace"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ")" ) "," (Set ($#k3_topmetr :::"R^1"::: ) ) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "a")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "b"))) & (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Var "g")))) "holds" (Bool (Set (Var "g")) "is" ($#v1_fcont_1 :::"continuous"::: ) )))) ; definitionlet "s" be ($#m1_subset_1 :::"Point":::) "of" (Set ($#k3_topmetr :::"R^1"::: ) ); let "r" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; :: original: :::"+"::: redefine func "s" :::"+"::: "r" -> ($#m1_subset_1 :::"Point":::) "of" (Set ($#k3_topmetr :::"R^1"::: ) ); end; definitionlet "s" be ($#m1_subset_1 :::"Point":::) "of" (Set ($#k3_topmetr :::"R^1"::: ) ); let "r" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; :: original: :::"-"::: redefine func "s" :::"-"::: "r" -> ($#m1_subset_1 :::"Point":::) "of" (Set ($#k3_topmetr :::"R^1"::: ) ); end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "X")) "," (Set ($#k3_topmetr :::"R^1"::: ) ); let "r" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; :: original: :::"+"::: redefine func "f" :::"+"::: "r" -> ($#m1_subset_1 :::"Function":::) "of" "X" "," (Set ($#k3_topmetr :::"R^1"::: ) ); end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "X")) "," (Set ($#k3_topmetr :::"R^1"::: ) ); let "r" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; :: original: :::"-"::: redefine func "f" :::"-"::: "r" -> ($#m1_subset_1 :::"Function":::) "of" "X" "," (Set ($#k3_topmetr :::"R^1"::: ) ); end; definitionlet "s", "t" be ($#m1_subset_1 :::"Point":::) "of" (Set ($#k3_topmetr :::"R^1"::: ) ); let "f" be ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Const "s")) "," (Set (Const "t")); let "r" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; :: original: :::"+"::: redefine func "f" :::"+"::: "r" -> ($#m1_borsuk_2 :::"Path"::: ) "of" (Set "s" ($#k2_borsuk_7 :::"+"::: ) "r") "," (Set "t" ($#k2_borsuk_7 :::"+"::: ) "r"); :: original: :::"-"::: redefine func "f" :::"-"::: "r" -> ($#m1_borsuk_2 :::"Path"::: ) "of" (Set "s" ($#k3_borsuk_7 :::"-"::: ) "r") "," (Set "t" ($#k3_borsuk_7 :::"-"::: ) "r"); end; definitionfunc :::"c[100]"::: -> ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k8_toprealb :::"Tunit_circle"::: ) (Num 3) ")" ) equals :: BORSUK_7:def 3 (Set ($#k4_euclid_5 :::"|["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k4_euclid_5 :::"]|"::: ) ); end; :: deftheorem defines :::"c[100]"::: BORSUK_7:def 3 : (Bool (Set ($#k8_borsuk_7 :::"c[100]"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k4_euclid_5 :::"|["::: ) (Num 1) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k4_euclid_5 :::"]|"::: ) )); definitionfunc :::"c[-100]"::: -> ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k8_toprealb :::"Tunit_circle"::: ) (Num 3) ")" ) equals :: BORSUK_7:def 4 (Set ($#k4_euclid_5 :::"|["::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k4_euclid_5 :::"]|"::: ) ); end; :: deftheorem defines :::"c[-100]"::: BORSUK_7:def 4 : (Bool (Set ($#k9_borsuk_7 :::"c[-100]"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k4_euclid_5 :::"|["::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k4_euclid_5 :::"]|"::: ) )); theorem :: BORSUK_7:40 (Bool (Set ($#k30_valued_1 :::"-"::: ) (Set ($#k8_borsuk_7 :::"c[100]"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k9_borsuk_7 :::"c[-100]"::: ) )) ; theorem :: BORSUK_7:41 (Bool (Set ($#k30_valued_1 :::"-"::: ) (Set ($#k9_borsuk_7 :::"c[-100]"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k8_borsuk_7 :::"c[100]"::: ) )) ; theorem :: BORSUK_7:42 (Bool (Set (Set ($#k8_borsuk_7 :::"c[100]"::: ) ) ($#k45_valued_1 :::"-"::: ) (Set ($#k9_borsuk_7 :::"c[-100]"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_euclid_5 :::"|["::: ) (Num 2) "," (Set ($#k6_numbers :::"0"::: ) ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k4_euclid_5 :::"]|"::: ) )) ; theorem :: BORSUK_7:43 (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool "(" (Bool (Set (Set (Var "p")) ($#k17_euclid :::"`1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k12_euclid :::"|."::: ) (Set (Var "p")) ($#k12_euclid :::".|"::: ) ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set "(" ($#k3_euclid_3 :::"Arg"::: ) (Set (Var "p")) ")" ) ")" ))) & (Bool (Set (Set (Var "p")) ($#k18_euclid :::"`2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k12_euclid :::"|."::: ) (Set (Var "p")) ($#k12_euclid :::".|"::: ) ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" ($#k3_euclid_3 :::"Arg"::: ) (Set (Var "p")) ")" ) ")" ))) ")" )) ; theorem :: BORSUK_7:44 (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set ($#k1_euclid_3 :::"cpx2euc"::: ) (Set "(" (Set "(" (Set ($#k12_euclid :::"|."::: ) (Set (Var "p")) ($#k12_euclid :::".|"::: ) ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set "(" ($#k3_euclid_3 :::"Arg"::: ) (Set (Var "p")) ")" ) ")" ) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set "(" (Set ($#k12_euclid :::"|."::: ) (Set (Var "p")) ($#k12_euclid :::".|"::: ) ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" ($#k3_euclid_3 :::"Arg"::: ) (Set (Var "p")) ")" ) ")" ) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set ($#k7_complex1 :::""::: ) ) ")" ) ")" )))) ; theorem :: BORSUK_7:45 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set ($#k12_euclid :::"|."::: ) (Set (Var "p1")) ($#k12_euclid :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k12_euclid :::"|."::: ) (Set (Var "p2")) ($#k12_euclid :::".|"::: ) )) & (Bool (Set ($#k3_euclid_3 :::"Arg"::: ) (Set (Var "p1"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_euclid_3 :::"Arg"::: ) (Set (Var "p2")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k8_real_1 :::"*"::: ) (Set (Var "i")) ")" )))) "holds" (Bool (Set (Var "p1")) ($#r1_hidden :::"="::: ) (Set (Var "p2"))))) ; theorem :: BORSUK_7:46 (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Set ($#k12_toprealb :::"CircleMap"::: ) ) ($#k1_funct_1 :::"."::: ) (Set (Var "r"))))) "holds" (Bool (Set ($#k3_euclid_3 :::"Arg"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k4_int_1 :::"frac"::: ) (Set (Var "r")) ")" ))))) ; theorem :: BORSUK_7:47 (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 3) ")" ) (Bool "for" (Set (Var "u1")) "," (Set (Var "u2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Num 3) ")" ) "st" (Bool (Bool (Set (Var "u1")) ($#r1_hidden :::"="::: ) (Set (Var "p1"))) & (Bool (Set (Var "u2")) ($#r1_hidden :::"="::: ) (Set (Var "p2")))) "holds" (Bool (Set (Set "(" ($#k13_euclid :::"Pitag_dist"::: ) (Num 3) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "u1")) "," (Set (Var "u2")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set "(" (Set "(" (Set "(" (Set (Var "p1")) ($#k1_euclid_5 :::"`1"::: ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "p2")) ($#k1_euclid_5 :::"`1"::: ) ")" ) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "p1")) ($#k2_euclid_5 :::"`2"::: ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "p2")) ($#k2_euclid_5 :::"`2"::: ) ")" ) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "p1")) ($#k3_euclid_5 :::"`3"::: ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "p2")) ($#k3_euclid_5 :::"`3"::: ) ")" ) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ))))) ; theorem :: BORSUK_7:48 (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 3) ")" ) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Num 3) ")" ) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Var "e"))) & (Bool (Set (Set (Var "p")) ($#k3_euclid_5 :::"`3"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k4_card_3 :::"product"::: ) (Set "(" "(" (Num 1) "," (Num 2) "," (Num 3) ")" ($#k1_borsuk_7 :::"-->"::: ) "(" (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k1_euclid_5 :::"`1"::: ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "r")) ($#k13_complex1 :::"/"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Num 2) ")" ) ")" ) ")" ) "," (Set "(" (Set "(" (Set (Var "p")) ($#k1_euclid_5 :::"`1"::: ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "r")) ($#k13_complex1 :::"/"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k2_rcomp_1 :::".["::: ) ) "," (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k2_euclid_5 :::"`2"::: ) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "r")) ($#k13_complex1 :::"/"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Num 2) ")" ) ")" ) ")" ) "," (Set "(" (Set "(" (Set (Var "p")) ($#k2_euclid_5 :::"`2"::: ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set (Var "r")) ($#k13_complex1 :::"/"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Num 2) ")" ) ")" ) ")" ) ($#k2_rcomp_1 :::".["::: ) ) "," (Set ($#k1_tarski :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ) ")" ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "e")) "," (Set (Var "r")) ")" ))))) ; theorem :: BORSUK_7:49 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "c")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set ($#k2_complex2 :::"Rotate"::: ) "(" (Set (Var "c")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_complex2 :::"Rotate"::: ) "(" (Set (Var "c")) "," (Set "(" (Set (Var "s")) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k8_real_1 :::"*"::: ) (Set (Var "i")) ")" ) ")" ) ")" ))))) ; theorem :: BORSUK_7:50 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set ($#k1_jordan24 :::"Rotate"::: ) (Set (Var "s"))) ($#r2_funct_2 :::"="::: ) (Set ($#k1_jordan24 :::"Rotate"::: ) (Set "(" (Set (Var "s")) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k8_real_1 :::"*"::: ) (Set (Var "i")) ")" ) ")" ))))) ; theorem :: BORSUK_7:51 (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set "(" ($#k1_jordan24 :::"Rotate"::: ) (Set (Var "s")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "p")) ")" ) ($#k12_euclid :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k12_euclid :::"|."::: ) (Set (Var "p")) ($#k12_euclid :::".|"::: ) )))) ; theorem :: BORSUK_7:52 (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool (Set ($#k3_euclid_3 :::"Arg"::: ) (Set "(" (Set "(" ($#k1_jordan24 :::"Rotate"::: ) (Set (Var "s")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_comptrig :::"Arg"::: ) (Set "(" ($#k2_complex2 :::"Rotate"::: ) "(" (Set "(" ($#k2_euclid_3 :::"euc2cpx"::: ) (Set (Var "p")) ")" ) "," (Set (Var "s")) ")" ")" ))))) ; theorem :: BORSUK_7:53 (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" )))) "holds" (Bool "ex" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) "st" (Bool (Set ($#k3_euclid_3 :::"Arg"::: ) (Set "(" (Set "(" ($#k1_jordan24 :::"Rotate"::: ) (Set (Var "s")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "s")) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k3_euclid_3 :::"Arg"::: ) (Set (Var "p")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k8_real_1 :::"*"::: ) (Set (Var "i")) ")" )))))) ; theorem :: BORSUK_7:54 (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set (Set "(" ($#k1_jordan24 :::"Rotate"::: ) (Set (Var "s")) ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" )))) ; theorem :: BORSUK_7:55 (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Set "(" ($#k1_jordan24 :::"Rotate"::: ) (Set (Var "s")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" )))) "holds" (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ))))) ; theorem :: BORSUK_7:56 (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool (Set (Set "(" ($#k1_jordan24 :::"Rotate"::: ) (Set (Var "s")) ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set "(" ($#k1_jordan24 :::"Rotate"::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "s")) ")" ) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "p")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "p"))))) ; theorem :: BORSUK_7:57 (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set (Set "(" ($#k1_jordan24 :::"Rotate"::: ) (Set (Var "s")) ")" ) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k1_jordan24 :::"Rotate"::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "s")) ")" ) ")" )) ($#r2_funct_2 :::"="::: ) (Set ($#k3_struct_0 :::"id"::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" )))) ; theorem :: BORSUK_7:58 (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "holds" (Bool "(" (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k3_topreal9 :::"Sphere"::: ) "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) ")" ) "," (Set (Var "r")) ")" )) "iff" (Bool (Set (Set "(" ($#k1_jordan24 :::"Rotate"::: ) (Set (Var "s")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "p"))) ($#r2_hidden :::"in"::: ) (Set ($#k3_topreal9 :::"Sphere"::: ) "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) ")" ) "," (Set (Var "r")) ")" )) ")" )))) ; theorem :: BORSUK_7:59 (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#~v3_xxreal_0 "non" ($#v3_xxreal_0 :::"negative"::: ) ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set (Set "(" ($#k1_jordan24 :::"Rotate"::: ) (Set (Var "s")) ")" ) ($#k7_relset_1 :::".:"::: ) (Set "(" ($#k3_topreal9 :::"Sphere"::: ) "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) ")" ) "," (Set (Var "r")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_topreal9 :::"Sphere"::: ) "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) ")" ) "," (Set (Var "r")) ")" )))) ; definitionlet "r" be ($#v1_xreal_0 :::"real"::: ) ($#~v3_xxreal_0 "non" ($#v3_xxreal_0 :::"negative"::: ) ) ($#m1_hidden :::"number"::: ) ; let "s" be ($#m1_subset_1 :::"Real":::); func :::"RotateCircle"::: "(" "r" "," "s" ")" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k7_toprealb :::"Tcircle"::: ) "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) ")" ) "," "r" ")" ")" ) "," (Set "(" ($#k7_toprealb :::"Tcircle"::: ) "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) ")" ) "," "r" ")" ")" ) equals :: BORSUK_7:def 5 (Set (Set "(" ($#k1_jordan24 :::"Rotate"::: ) "s" ")" ) ($#k2_tmap_1 :::"|"::: ) (Set "(" ($#k7_toprealb :::"Tcircle"::: ) "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) ")" ) "," "r" ")" ")" )); end; :: deftheorem defines :::"RotateCircle"::: BORSUK_7:def 5 : (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#~v3_xxreal_0 "non" ($#v3_xxreal_0 :::"negative"::: ) ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set ($#k10_borsuk_7 :::"RotateCircle"::: ) "(" (Set (Var "r")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_jordan24 :::"Rotate"::: ) (Set (Var "s")) ")" ) ($#k2_tmap_1 :::"|"::: ) (Set "(" ($#k7_toprealb :::"Tcircle"::: ) "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) ")" ) "," (Set (Var "r")) ")" ")" ))))); registrationlet "r" be ($#v1_xreal_0 :::"real"::: ) ($#~v3_xxreal_0 "non" ($#v3_xxreal_0 :::"negative"::: ) ) ($#m1_hidden :::"number"::: ) ; let "s" be ($#m1_subset_1 :::"Real":::); cluster (Set ($#k10_borsuk_7 :::"RotateCircle"::: ) "(" "r" "," "s" ")" ) -> ($#v3_tops_2 :::"being_homeomorphism"::: ) ; end; theorem :: BORSUK_7:60 (Bool "for" (Set (Var "r2")) "," (Set (Var "r1")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" ) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"="::: ) (Set (Set ($#k12_toprealb :::"CircleMap"::: ) ) ($#k1_funct_1 :::"."::: ) (Set (Var "r2"))))) "holds" (Bool (Set (Set "(" ($#k10_borsuk_7 :::"RotateCircle"::: ) "(" (Num 1) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" ($#k3_euclid_3 :::"Arg"::: ) (Set (Var "p")) ")" ) ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set ($#k12_toprealb :::"CircleMap"::: ) ) ($#k1_funct_1 :::"."::: ) (Set (Var "r1")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set ($#k12_toprealb :::"CircleMap"::: ) ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "r1")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "r2")) ")" ))))) ; begin definitionlet "n" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::); let "p" be ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Const "n")) ")" ); let "r" be ($#v1_xreal_0 :::"real"::: ) ($#~v3_xxreal_0 "non" ($#v3_xxreal_0 :::"negative"::: ) ) ($#m1_hidden :::"number"::: ) ; func :::"CircleIso"::: "(" "p" "," "r" ")" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k8_toprealb :::"Tunit_circle"::: ) "n" ")" ) "," (Set "(" ($#k7_toprealb :::"Tcircle"::: ) "(" "p" "," "r" ")" ")" ) means :: BORSUK_7:def 6 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k8_toprealb :::"Tunit_circle"::: ) "n" ")" ) (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) "n" ")" ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b")))) "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "r" ($#k1_rlvect_1 :::"*"::: ) (Set (Var "b")) ")" ) ($#k3_rlvect_1 :::"+"::: ) "p")))); end; :: deftheorem defines :::"CircleIso"::: BORSUK_7:def 6 : (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#~v3_xxreal_0 "non" ($#v3_xxreal_0 :::"negative"::: ) ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "b4")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k8_toprealb :::"Tunit_circle"::: ) (Set (Var "n")) ")" ) "," (Set "(" ($#k7_toprealb :::"Tcircle"::: ) "(" (Set (Var "p")) "," (Set (Var "r")) ")" ")" ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k11_borsuk_7 :::"CircleIso"::: ) "(" (Set (Var "p")) "," (Set (Var "r")) ")" )) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k8_toprealb :::"Tunit_circle"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b")))) "holds" (Bool (Set (Set (Var "b4")) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "r")) ($#k1_rlvect_1 :::"*"::: ) (Set (Var "b")) ")" ) ($#k3_rlvect_1 :::"+"::: ) (Set (Var "p")))))) ")" ))))); registrationlet "n" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::); let "p" be ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Const "n")) ")" ); let "r" be ($#v1_xreal_0 :::"real"::: ) ($#v2_xxreal_0 :::"positive"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set ($#k11_borsuk_7 :::"CircleIso"::: ) "(" "p" "," "r" ")" ) -> ($#v3_tops_2 :::"being_homeomorphism"::: ) ; end; definitionfunc :::"SphereMap"::: -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k3_topmetr :::"R^1"::: ) ) "," (Set "(" ($#k8_toprealb :::"Tunit_circle"::: ) (Num 3) ")" ) means :: BORSUK_7:def 7 (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_euclid_5 :::"|["::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) "," (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k4_euclid_5 :::"]|"::: ) ))); end; :: deftheorem defines :::"SphereMap"::: BORSUK_7:def 7 : (Bool "for" (Set (Var "b1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k3_topmetr :::"R^1"::: ) ) "," (Set "(" ($#k8_toprealb :::"Tunit_circle"::: ) (Num 3) ")" ) "holds" (Bool "(" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set ($#k12_borsuk_7 :::"SphereMap"::: ) )) "iff" (Bool "for" (Set (Var "x")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "b1")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_euclid_5 :::"|["::: ) (Set "(" ($#k21_sin_cos :::"cos"::: ) (Set "(" (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) "," (Set "(" ($#k18_sin_cos :::"sin"::: ) (Set "(" (Set "(" (Num 2) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) ($#k8_real_1 :::"*"::: ) (Set (Var "x")) ")" ) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k4_euclid_5 :::"]|"::: ) ))) ")" )); theorem :: BORSUK_7:61 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"Integer":::) "holds" (Bool (Set (Set ($#k12_borsuk_7 :::"SphereMap"::: ) ) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k8_borsuk_7 :::"c[100]"::: ) ))) ; registration cluster (Set ($#k12_borsuk_7 :::"SphereMap"::: ) ) -> ($#v5_pre_topc :::"continuous"::: ) ; end; definitionlet "r" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; func :::"eLoop"::: "r" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k17_borsuk_1 :::"I[01]"::: ) ) "," (Set "(" ($#k8_toprealb :::"Tunit_circle"::: ) (Num 3) ")" ) means :: BORSUK_7:def 8 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k17_borsuk_1 :::"I[01]"::: ) ) "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_euclid_5 :::"|["::: ) (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")) ")" ) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k4_euclid_5 :::"]|"::: ) ))); end; :: deftheorem defines :::"eLoop"::: BORSUK_7:def 8 : (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 ($#k17_borsuk_1 :::"I[01]"::: ) ) "," (Set "(" ($#k8_toprealb :::"Tunit_circle"::: ) (Num 3) ")" ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k13_borsuk_7 :::"eLoop"::: ) (Set (Var "r")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set ($#k17_borsuk_1 :::"I[01]"::: ) ) "holds" (Bool (Set (Set (Var "b2")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k4_euclid_5 :::"|["::: ) (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")) ")" ) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k4_euclid_5 :::"]|"::: ) ))) ")" ))); theorem :: BORSUK_7:62 (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k13_borsuk_7 :::"eLoop"::: ) (Set (Var "r"))) ($#r2_funct_2 :::"="::: ) (Set (Set ($#k12_borsuk_7 :::"SphereMap"::: ) ) ($#k1_topalg_3 :::"*"::: ) (Set "(" ($#k2_topalg_5 :::"ExtendInt"::: ) (Set (Var "r")) ")" )))) ; definitionlet "i" be ($#m1_hidden :::"Integer":::); :: original: :::"eLoop"::: redefine func :::"eLoop"::: "i" -> ($#m1_borsuk_2 :::"Loop":::) "of" (Set ($#k8_borsuk_7 :::"c[100]"::: ) ); end; registrationlet "i" be ($#m1_hidden :::"Integer":::); cluster (Set ($#k13_borsuk_7 :::"eLoop"::: ) "i") -> ($#v3_topalg_6 :::"nullhomotopic"::: ) for ($#m1_borsuk_2 :::"Loop":::) "of" (Set ($#k8_borsuk_7 :::"c[100]"::: ) ); end; theorem :: BORSUK_7:63 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" )))) "holds" (Bool (Set ($#k12_euclid :::"|."::: ) (Set "(" (Set (Var "p")) ($#k10_toprealc :::"(/)"::: ) (Set ($#k12_euclid :::"|."::: ) (Set (Var "p")) ($#k12_euclid :::".|"::: ) ) ")" ) ($#k12_euclid :::".|"::: ) ) ($#r1_hidden :::"="::: ) (Num 1)))) ; definitionlet "n" be ($#m1_hidden :::"Nat":::); let "p" be ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Const "n")) ")" ); assume (Bool (Set (Const "p")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Const "n")) ")" ))) ; func :::"Rn->S1"::: "p" -> ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k7_toprealb :::"Tcircle"::: ) "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) "n" ")" ) ")" ) "," (Num 1) ")" ")" ) equals :: BORSUK_7:def 9 (Set "p" ($#k10_toprealc :::"(/)"::: ) (Set ($#k12_euclid :::"|."::: ) "p" ($#k12_euclid :::".|"::: ) )); end; :: deftheorem defines :::"Rn->S1"::: BORSUK_7:def 9 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "p")) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" )))) "holds" (Bool (Set ($#k15_borsuk_7 :::"Rn->S1"::: ) (Set (Var "p"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k10_toprealc :::"(/)"::: ) (Set ($#k12_euclid :::"|."::: ) (Set (Var "p")) ($#k12_euclid :::".|"::: ) ))))); definitionlet "n" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m1_hidden :::"Nat":::); let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k7_toprealb :::"Tcircle"::: ) "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set "(" (Set (Const "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) "," (Num 1) ")" ")" ) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Const "n")) ")" ); func :::"Sn1->Sn"::: "f" -> ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k8_toprealb :::"Tunit_circle"::: ) (Set "(" "n" ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" ($#k8_toprealb :::"Tunit_circle"::: ) "n" ")" ) means :: BORSUK_7:def 10 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k7_toprealb :::"Tcircle"::: ) "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set "(" "n" ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) "," (Num 1) ")" ")" ) "st" (Bool (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k30_valued_1 :::"-"::: ) (Set (Var "x"))))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k15_borsuk_7 :::"Rn->S1"::: ) (Set "(" (Set "(" "f" ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" "f" ($#k3_funct_2 :::"."::: ) (Set (Var "y")) ")" ) ")" )))); end; :: deftheorem defines :::"Sn1->Sn"::: BORSUK_7:def 10 : (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k7_toprealb :::"Tcircle"::: ) "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) "," (Num 1) ")" ")" ) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "b3")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k8_toprealb :::"Tunit_circle"::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) "," (Set "(" ($#k8_toprealb :::"Tunit_circle"::: ) (Set (Var "n")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k16_borsuk_7 :::"Sn1->Sn"::: ) (Set (Var "f")))) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k7_toprealb :::"Tcircle"::: ) "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) "," (Num 1) ")" ")" ) "st" (Bool (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set ($#k30_valued_1 :::"-"::: ) (Set (Var "x"))))) "holds" (Bool (Set (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k15_borsuk_7 :::"Rn->S1"::: ) (Set "(" (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k5_algstr_0 :::"-"::: ) (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "y")) ")" ) ")" )))) ")" )))); definitionlet "x0", "y0" be ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k8_toprealb :::"Tunit_circle"::: ) (Num 2) ")" ); let "xt" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_borsuk_2 :::"Path"::: ) "of" (Set (Const "x0")) "," (Set (Const "y0")); assume (Bool (Set (Const "xt")) ($#r2_hidden :::"in"::: ) (Set (Set ($#k12_toprealb :::"CircleMap"::: ) ) ($#k8_relset_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Const "x0")) ($#k1_tarski :::"}"::: ) ))) ; func :::"liftPath"::: "(" "f" "," "xt" ")" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k17_borsuk_1 :::"I[01]"::: ) ) "," (Set ($#k3_topmetr :::"R^1"::: ) ) means :: BORSUK_7:def 11 (Bool "(" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) "xt") & (Bool "f" ($#r2_funct_2 :::"="::: ) (Set (Set ($#k12_toprealb :::"CircleMap"::: ) ) ($#k1_partfun1 :::"*"::: ) it)) & (Bool it "is" ($#v5_pre_topc :::"continuous"::: ) ) & (Bool "(" "for" (Set (Var "f1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k17_borsuk_1 :::"I[01]"::: ) ) "," (Set ($#k3_topmetr :::"R^1"::: ) ) "st" (Bool (Bool (Set (Var "f1")) "is" ($#v5_pre_topc :::"continuous"::: ) ) & (Bool "f" ($#r2_funct_2 :::"="::: ) (Set (Set ($#k12_toprealb :::"CircleMap"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set (Var "f1")))) & (Bool (Set (Set (Var "f1")) ($#k1_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) "xt")) "holds" (Bool it ($#r2_funct_2 :::"="::: ) (Set (Var "f1"))) ")" ) ")" ); end; :: deftheorem defines :::"liftPath"::: BORSUK_7:def 11 : (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_hidden :::"set"::: ) (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 ($#k1_tarski :::"{"::: ) (Set (Var "x0")) ($#k1_tarski :::"}"::: ) )))) "holds" (Bool "for" (Set (Var "b5")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k17_borsuk_1 :::"I[01]"::: ) ) "," (Set ($#k3_topmetr :::"R^1"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k17_borsuk_7 :::"liftPath"::: ) "(" (Set (Var "f")) "," (Set (Var "xt")) ")" )) "iff" (Bool "(" (Bool (Set (Set (Var "b5")) ($#k1_funct_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 "b5")))) & (Bool (Set (Var "b5")) "is" ($#v5_pre_topc :::"continuous"::: ) ) & (Bool "(" "for" (Set (Var "f1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k17_borsuk_1 :::"I[01]"::: ) ) "," (Set ($#k3_topmetr :::"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_funct_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "xt")))) "holds" (Bool (Set (Var "b5")) ($#r2_funct_2 :::"="::: ) (Set (Var "f1"))) ")" ) ")" ) ")" ))))); definitionlet "n" be ($#m1_hidden :::"Nat":::); let "p", "x", "y" be ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Const "n")) ")" ); let "r" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; pred "x" "," "y" :::"are_antipodals_of"::: "p" "," "r" means :: BORSUK_7:def 12 (Bool "(" (Bool "x" "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k7_toprealb :::"Tcircle"::: ) "(" "p" "," "r" ")" ")" )) & (Bool "y" "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k7_toprealb :::"Tcircle"::: ) "(" "p" "," "r" ")" ")" )) & (Bool "p" ($#r2_hidden :::"in"::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" "x" "," "y" ")" )) ")" ); end; :: deftheorem defines :::"are_antipodals_of"::: BORSUK_7:def 12 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "," (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r1_borsuk_7 :::"are_antipodals_of"::: ) (Set (Var "p")) "," (Set (Var "r"))) "iff" (Bool "(" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k7_toprealb :::"Tcircle"::: ) "(" (Set (Var "p")) "," (Set (Var "r")) ")" ")" )) & (Bool (Set (Var "y")) "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k7_toprealb :::"Tcircle"::: ) "(" (Set (Var "p")) "," (Set (Var "r")) ")" ")" )) & (Bool (Set (Var "p")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rltopsp1 :::"LSeg"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" )) ")" ) ")" )))); definitionlet "n" be ($#m1_hidden :::"Nat":::); let "p", "x", "y" be ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Const "n")) ")" ); let "r" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; let "f" be ($#m1_hidden :::"Function":::); pred "x" "," "y" :::"are_antipodals_of"::: "p" "," "r" "," "f" means :: BORSUK_7:def 13 (Bool "(" (Bool "x" "," "y" ($#r1_borsuk_7 :::"are_antipodals_of"::: ) "p" "," "r") & (Bool "x" ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "f")) & (Bool "y" ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "f")) & (Bool (Set "f" ($#k1_funct_1 :::"."::: ) "x") ($#r1_hidden :::"="::: ) (Set "f" ($#k1_funct_1 :::"."::: ) "y")) ")" ); end; :: deftheorem defines :::"are_antipodals_of"::: BORSUK_7:def 13 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "," (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r2_borsuk_7 :::"are_antipodals_of"::: ) (Set (Var "p")) "," (Set (Var "r")) "," (Set (Var "f"))) "iff" (Bool "(" (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r1_borsuk_7 :::"are_antipodals_of"::: ) (Set (Var "p")) "," (Set (Var "r"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "y")))) ")" ) ")" ))))); definitionlet "m", "n" be ($#m1_hidden :::"Nat":::); let "p" be ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Const "m")) ")" ); let "r" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k7_toprealb :::"Tcircle"::: ) "(" (Set (Const "p")) "," (Set (Const "r")) ")" ")" ) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Const "n")) ")" ); attr "f" is :::"with_antipodals"::: means :: BORSUK_7:def 14 (Bool "ex" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) "m" ")" ) "st" (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r2_borsuk_7 :::"are_antipodals_of"::: ) "p" "," "r" "," "f")); end; :: deftheorem defines :::"with_antipodals"::: BORSUK_7:def 14 : (Bool "for" (Set (Var "m")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "m")) ")" ) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k7_toprealb :::"Tcircle"::: ) "(" (Set (Var "p")) "," (Set (Var "r")) ")" ")" ) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v2_borsuk_7 :::"with_antipodals"::: ) ) "iff" (Bool "ex" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "m")) ")" ) "st" (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r2_borsuk_7 :::"are_antipodals_of"::: ) (Set (Var "p")) "," (Set (Var "r")) "," (Set (Var "f")))) ")" ))))); notationlet "m", "n" be ($#m1_hidden :::"Nat":::); let "p" be ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Const "m")) ")" ); let "r" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k7_toprealb :::"Tcircle"::: ) "(" (Set (Const "p")) "," (Set (Const "r")) ")" ")" ) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Const "n")) ")" ); antonym :::"without_antipodals"::: "f" for :::"with_antipodals"::: ; end; theorem :: BORSUK_7:64 (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#~v3_xxreal_0 "non" ($#v3_xxreal_0 :::"negative"::: ) ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k7_toprealb :::"Tcircle"::: ) "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) ")" ) "," (Set (Var "r")) ")" ")" ))) "holds" (Bool (Set (Var "x")) "," (Set ($#k4_algstr_0 :::"-"::: ) (Set (Var "x"))) ($#r1_borsuk_7 :::"are_antipodals_of"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" )) "," (Set (Var "r")))))) ; theorem :: BORSUK_7:65 (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p")) "," (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "x1")) "," (Set (Var "y1")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#v2_xxreal_0 :::"positive"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "x")) "," (Set (Var "y")) ($#r1_borsuk_7 :::"are_antipodals_of"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" )) "," (Num 1)) & (Bool (Set (Var "x1")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k11_borsuk_7 :::"CircleIso"::: ) "(" (Set (Var "p")) "," (Set (Var "r")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) & (Bool (Set (Var "y1")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k11_borsuk_7 :::"CircleIso"::: ) "(" (Set (Var "p")) "," (Set (Var "r")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "y"))))) "holds" (Bool (Set (Var "x1")) "," (Set (Var "y1")) ($#r1_borsuk_7 :::"are_antipodals_of"::: ) (Set (Var "p")) "," (Set (Var "r")))))) ; theorem :: BORSUK_7:66 (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k7_toprealb :::"Tcircle"::: ) "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) "," (Num 1) ")" ")" ) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k7_toprealb :::"Tcircle"::: ) "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) "," (Num 1) ")" ")" ) "st" (Bool (Bool (Set (Var "f")) "is" ($#v2_borsuk_7 :::"without_antipodals"::: ) )) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k45_valued_1 :::"-"::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k30_valued_1 :::"-"::: ) (Set (Var "x")) ")" ) ")" )) ($#r1_hidden :::"<>"::: ) (Set ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" )))))) ; theorem :: BORSUK_7:67 (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k7_toprealb :::"Tcircle"::: ) "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) "," (Num 1) ")" ")" ) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "f")) "is" ($#v2_borsuk_7 :::"without_antipodals"::: ) )) "holds" (Bool (Set ($#k16_borsuk_7 :::"Sn1->Sn"::: ) (Set (Var "f"))) "is" ($#v1_borsuk_7 :::"odd"::: ) ))) ; theorem :: BORSUK_7:68 (Bool "for" (Set (Var "n")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "B1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k7_toprealb :::"Tcircle"::: ) "(" (Set "(" ($#k4_struct_0 :::"0."::: ) (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ) ")" ) "," (Num 1) ")" ")" ) "," (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k20_valued_2 :::"(-)"::: ) )) & (Bool (Set (Var "B1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k80_valued_2 :::"<-->"::: ) (Set (Var "g")))) & (Bool (Set (Var "f")) "is" ($#v2_borsuk_7 :::"without_antipodals"::: ) )) "holds" (Bool (Set ($#k16_borsuk_7 :::"Sn1->Sn"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "B1")) ($#k70_valued_2 :::""::: ) (Set "(" (Set "(" (Set (Var "n")) ($#k1_jgraph_4 :::"NormF"::: ) ")" ) ($#k1_partfun1 :::"*"::: ) (Set (Var "B1")) ")" ))))) ; registrationlet "n" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m1_hidden :::"Nat":::); let "r" be ($#v1_xreal_0 :::"real"::: ) ($#v3_xxreal_0 :::"negative"::: ) ($#m1_hidden :::"number"::: ) ; let "p" be ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set "(" (Set (Const "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" ) ")" ); cluster ($#v1_funct_1 :::"Function-like"::: ) ($#v1_funct_2 :::"quasi_total"::: ) -> ($#v2_borsuk_7 :::"without_antipodals"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k7_toprealb :::"Tcircle"::: ) "(" "p" "," "r" ")" ")" )) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) "n" ")" )) ($#k2_zfmisc_1 :::":]"::: ) )); end; registrationlet "r" be ($#v1_xreal_0 :::"real"::: ) ($#~v3_xxreal_0 "non" ($#v3_xxreal_0 :::"negative"::: ) ) ($#m1_hidden :::"number"::: ) ; let "p" be ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 3) ")" ); cluster ($#v1_funct_1 :::"Function-like"::: ) ($#v1_funct_2 :::"quasi_total"::: ) ($#v5_pre_topc :::"continuous"::: ) -> ($#v2_borsuk_7 :::"with_antipodals"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k7_toprealb :::"Tcircle"::: ) "(" "p" "," "r" ")" ")" )) "," (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Num 2) ")" )) ($#k2_zfmisc_1 :::":]"::: ) )); end;