:: EUCLID_9 semantic presentation begin registrationlet "s" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; let "r" be ($#~v2_xxreal_0 "non" ($#v2_xxreal_0 :::"positive"::: ) ) ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set bbbadK4_XXREAL_1((Set "(" "s" ($#k6_xcmplx_0 :::"-"::: ) "r" ")" ) "," (Set "(" "s" ($#k2_xcmplx_0 :::"+"::: ) "r" ")" ))) -> ($#v1_xboole_0 :::"empty"::: ) ; cluster (Set bbbadK2_XXREAL_1((Set "(" "s" ($#k6_xcmplx_0 :::"-"::: ) "r" ")" ) "," (Set "(" "s" ($#k2_xcmplx_0 :::"+"::: ) "r" ")" ))) -> ($#v1_xboole_0 :::"empty"::: ) ; cluster (Set bbbadK3_XXREAL_1((Set "(" "s" ($#k6_xcmplx_0 :::"-"::: ) "r" ")" ) "," (Set "(" "s" ($#k2_xcmplx_0 :::"+"::: ) "r" ")" ))) -> ($#v1_xboole_0 :::"empty"::: ) ; end; registrationlet "s" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; let "r" be ($#v3_xxreal_0 :::"negative"::: ) ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set bbbadK1_XXREAL_1((Set "(" "s" ($#k6_xcmplx_0 :::"-"::: ) "r" ")" ) "," (Set "(" "s" ($#k2_xcmplx_0 :::"+"::: ) "r" ")" ))) -> ($#v1_xboole_0 :::"empty"::: ) ; end; registrationlet "n" be ($#m1_hidden :::"Nat":::); let "f" be ($#v1_valued_0 :::"complex-valued"::: ) (Set (Const "n")) ($#v3_card_1 :::"-element"::: ) ($#m1_hidden :::"FinSequence":::); cluster (Set ($#k30_valued_1 :::"-"::: ) "f") -> "n" ($#v3_card_1 :::"-element"::: ) ; cluster (Set "f" ($#k35_valued_1 :::"""::: ) ) -> "n" ($#v3_card_1 :::"-element"::: ) ; cluster (Set "f" ($#k39_valued_1 :::"^2"::: ) ) -> "n" ($#v3_card_1 :::"-element"::: ) ; cluster (Set ($#k54_valued_1 :::"|."::: ) "f" ($#k54_valued_1 :::".|"::: ) ) -> "n" ($#v3_card_1 :::"-element"::: ) ; let "g" be ($#v1_valued_0 :::"complex-valued"::: ) (Set (Const "n")) ($#v3_card_1 :::"-element"::: ) ($#m1_hidden :::"FinSequence":::); cluster (Set "f" ($#k1_valued_1 :::"+"::: ) "g") -> "n" ($#v3_card_1 :::"-element"::: ) ; cluster (Set "f" ($#k45_valued_1 :::"-"::: ) "g") -> "n" ($#v3_card_1 :::"-element"::: ) ; cluster (Set "f" ($#k18_valued_1 :::"(#)"::: ) "g") -> "n" ($#v3_card_1 :::"-element"::: ) ; cluster (Set "f" ($#k50_valued_1 :::"/""::: ) "g") -> "n" ($#v3_card_1 :::"-element"::: ) ; end; registrationlet "c" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; let "n" be ($#m1_hidden :::"Nat":::); let "f" be ($#v1_valued_0 :::"complex-valued"::: ) (Set (Const "n")) ($#v3_card_1 :::"-element"::: ) ($#m1_hidden :::"FinSequence":::); cluster (Set "c" ($#k7_valued_1 :::"+"::: ) "f") -> "n" ($#v3_card_1 :::"-element"::: ) ; cluster (Set "f" ($#k13_valued_1 :::"-"::: ) "c") -> "n" ($#v3_card_1 :::"-element"::: ) ; cluster (Set "c" ($#k24_valued_1 :::"(#)"::: ) "f") -> "n" ($#v3_card_1 :::"-element"::: ) ; end; registrationlet "f" be ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"Function":::); cluster (Set ($#k1_tarski :::"{"::: ) "f" ($#k1_tarski :::"}"::: ) ) -> ($#v3_valued_2 :::"real-functions-membered"::: ) ; let "g" be ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"Function":::); cluster (Set ($#k2_tarski :::"{"::: ) "f" "," "g" ($#k2_tarski :::"}"::: ) ) -> ($#v3_valued_2 :::"real-functions-membered"::: ) ; end; registrationlet "n" be ($#m1_hidden :::"Nat":::); let "x", "y" be ($#m1_hidden :::"set"::: ) ; let "f" be (Set (Const "n")) ($#v3_card_1 :::"-element"::: ) ($#m1_hidden :::"FinSequence":::); cluster (Set "f" ($#k2_funct_7 :::"+*"::: ) "(" "x" "," "y" ")" ) -> "n" ($#v3_card_1 :::"-element"::: ) ; end; theorem :: EUCLID_9:1 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "f")) "being" (Set (Var "b1")) ($#v3_card_1 :::"-element"::: ) ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "f")) "is" ($#v1_xboole_0 :::"empty"::: ) )) "holds" (Bool (Set (Var "n")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )))) ; theorem :: EUCLID_9:2 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "f")) "being" ($#v3_valued_0 :::"real-valued"::: ) (Set (Var "b1")) ($#v3_card_1 :::"-element"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k1_euclid :::"REAL"::: ) (Set (Var "n")))))) ; theorem :: EUCLID_9:3 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k54_valued_1 :::"abs"::: ) (Set "(" (Set (Var "f")) ($#k45_valued_1 :::"-"::: ) (Set (Var "g")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k54_valued_1 :::"abs"::: ) (Set "(" (Set (Var "g")) ($#k45_valued_1 :::"-"::: ) (Set (Var "f")) ")" )))) ; definitionlet "n" be ($#m1_hidden :::"Nat":::); let "f1", "f2" be ($#v3_valued_0 :::"real-valued"::: ) (Set (Const "n")) ($#v3_card_1 :::"-element"::: ) ($#m1_hidden :::"FinSequence":::); func :::"max_diff_index"::: "(" "f1" "," "f2" ")" -> ($#m1_hidden :::"Nat":::) equals :: EUCLID_9:def 1 "the" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set "(" ($#k3_euclid :::"abs"::: ) (Set "(" "f1" ($#k8_rvsum_1 :::"-"::: ) "f2" ")" ) ")" ) ($#k8_relset_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k1_xxreal_2 :::"sup"::: ) (Set "(" ($#k1_rvsum_1 :::"rng"::: ) (Set "(" ($#k3_euclid :::"abs"::: ) (Set "(" "f1" ($#k8_rvsum_1 :::"-"::: ) "f2" ")" ) ")" ) ")" ) ")" ) ($#k1_tarski :::"}"::: ) )); commutativity (Bool "for" (Set (Var "b1")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#v3_valued_0 :::"real-valued"::: ) (Set (Const "n")) ($#v3_card_1 :::"-element"::: ) ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) "the" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set "(" ($#k3_euclid :::"abs"::: ) (Set "(" (Set (Var "f1")) ($#k8_rvsum_1 :::"-"::: ) (Set (Var "f2")) ")" ) ")" ) ($#k8_relset_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k1_xxreal_2 :::"sup"::: ) (Set "(" ($#k1_rvsum_1 :::"rng"::: ) (Set "(" ($#k3_euclid :::"abs"::: ) (Set "(" (Set (Var "f1")) ($#k8_rvsum_1 :::"-"::: ) (Set (Var "f2")) ")" ) ")" ) ")" ) ")" ) ($#k1_tarski :::"}"::: ) )))) "holds" (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) "the" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set "(" ($#k3_euclid :::"abs"::: ) (Set "(" (Set (Var "f2")) ($#k8_rvsum_1 :::"-"::: ) (Set (Var "f1")) ")" ) ")" ) ($#k8_relset_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k1_xxreal_2 :::"sup"::: ) (Set "(" ($#k1_rvsum_1 :::"rng"::: ) (Set "(" ($#k3_euclid :::"abs"::: ) (Set "(" (Set (Var "f2")) ($#k8_rvsum_1 :::"-"::: ) (Set (Var "f1")) ")" ) ")" ) ")" ) ")" ) ($#k1_tarski :::"}"::: ) ))))) ; end; :: deftheorem defines :::"max_diff_index"::: EUCLID_9:def 1 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#v3_valued_0 :::"real-valued"::: ) (Set (Var "b1")) ($#v3_card_1 :::"-element"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set ($#k1_euclid_9 :::"max_diff_index"::: ) "(" (Set (Var "f1")) "," (Set (Var "f2")) ")" ) ($#r1_hidden :::"="::: ) "the" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set "(" ($#k3_euclid :::"abs"::: ) (Set "(" (Set (Var "f1")) ($#k8_rvsum_1 :::"-"::: ) (Set (Var "f2")) ")" ) ")" ) ($#k8_relset_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k1_xxreal_2 :::"sup"::: ) (Set "(" ($#k1_rvsum_1 :::"rng"::: ) (Set "(" ($#k3_euclid :::"abs"::: ) (Set "(" (Set (Var "f1")) ($#k8_rvsum_1 :::"-"::: ) (Set (Var "f2")) ")" ) ")" ) ")" ) ")" ) ($#k1_tarski :::"}"::: ) ))))); theorem :: EUCLID_9:4 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#v3_valued_0 :::"real-valued"::: ) (Set (Var "b1")) ($#v3_card_1 :::"-element"::: ) ($#m1_hidden :::"FinSequence":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k1_euclid_9 :::"max_diff_index"::: ) "(" (Set (Var "f1")) "," (Set (Var "f2")) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f1")))))) ; theorem :: EUCLID_9:5 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#v3_valued_0 :::"real-valued"::: ) (Set (Var "b2")) ($#v3_card_1 :::"-element"::: ) ($#m1_hidden :::"FinSequence":::) "holds" (Bool (Set (Set "(" ($#k3_euclid :::"abs"::: ) (Set "(" (Set (Var "f1")) ($#k8_rvsum_1 :::"-"::: ) (Set (Var "f2")) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k3_euclid :::"abs"::: ) (Set "(" (Set (Var "f1")) ($#k8_rvsum_1 :::"-"::: ) (Set (Var "f2")) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_euclid_9 :::"max_diff_index"::: ) "(" (Set (Var "f1")) "," (Set (Var "f2")) ")" ")" )))))) ; registration cluster (Set ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set "(" ($#k14_euclid :::"Euclid"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) -> ($#v7_struct_0 :::"trivial"::: ) ; end; registrationlet "n" be ($#m1_hidden :::"Nat":::); cluster (Set ($#k14_euclid :::"Euclid"::: ) "n") -> ($#v2_monoid_0 :::"constituted-FinSeqs"::: ) ; end; registrationlet "n" be ($#m1_hidden :::"Nat":::); cluster -> (Set ($#k1_numbers :::"REAL"::: ) ) ($#v5_relat_1 :::"-valued"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) "n" ")" )); end; registrationlet "n" be ($#m1_hidden :::"Nat":::); cluster -> "n" ($#v3_card_1 :::"-element"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) "n" ")" )); end; theorem :: EUCLID_9:6 (Bool (Set ($#k2_pcomps_1 :::"Family_open_set"::: ) (Set "(" ($#k14_euclid :::"Euclid"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ) ($#k2_tarski :::"}"::: ) )) ; theorem :: EUCLID_9:7 (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) "holds" (Bool "(" (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "or" (Bool (Set (Var "B")) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) )) ")" )) ; definitionlet "n" be ($#m1_hidden :::"Nat":::); let "e" be ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Set (Const "n")) ")" ); func :::"@"::: "e" -> ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set "(" ($#k14_euclid :::"Euclid"::: ) "n" ")" ) ")" ) equals :: EUCLID_9:def 2 "e"; end; :: deftheorem defines :::"@"::: EUCLID_9:def 2 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set ($#k2_euclid_9 :::"@"::: ) (Set (Var "e"))) ($#r1_hidden :::"="::: ) (Set (Var "e"))))); registrationlet "n" be ($#m1_hidden :::"Nat":::); let "e" be ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Set (Const "n")) ")" ); let "r" be ($#~v2_xxreal_0 "non" ($#v2_xxreal_0 :::"positive"::: ) ) ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set ($#k9_metric_1 :::"Ball"::: ) "(" "e" "," "r" ")" ) -> ($#v1_xboole_0 :::"empty"::: ) ; end; registrationlet "n" be ($#m1_hidden :::"Nat":::); let "e" be ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Set (Const "n")) ")" ); let "r" be ($#v2_xxreal_0 :::"positive"::: ) ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set ($#k9_metric_1 :::"Ball"::: ) "(" "e" "," "r" ")" ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: EUCLID_9:8 (Bool "for" (Set (Var "n")) "," (Set (Var "i")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "p1")) "," (Set (Var "p2")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "p1"))))) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "p1")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "p2")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i")) ")" ) ")" ) ($#k5_square_1 :::"^2"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set "(" ($#k12_rvsum_1 :::"sqr"::: ) (Set "(" (Set (Var "p1")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "p2")) ")" ) ")" ))))) ; theorem :: EUCLID_9:9 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "o")) "," (Set (Var "p")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set "(" ($#k15_euclid :::"TOP-REAL"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k1_topreal9 :::"Ball"::: ) "(" (Set (Var "o")) "," (Set (Var "r")) ")" ))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k5_algstr_0 :::"-"::: ) (Set (Var "o")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set (Var "o")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) ")" ))))) ; theorem :: EUCLID_9:10 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "a")) "," (Set (Var "o")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "o")) "," (Set (Var "r")) ")" ))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k8_rvsum_1 :::"-"::: ) (Set (Var "o")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set "(" (Set "(" (Set (Var "a")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set (Var "o")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) ")" ))))) ; definitionlet "f" be ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"Function":::); let "r" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; func :::"Intervals"::: "(" "f" "," "r" ")" -> ($#m1_hidden :::"Function":::) means :: EUCLID_9:def 3 (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "f")) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "f"))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" (Set "(" "f" ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) "r" ")" ) "," (Set "(" (Set "(" "f" ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) "r" ")" ) ($#k2_rcomp_1 :::".["::: ) )) ")" ) ")" ); end; :: deftheorem defines :::"Intervals"::: EUCLID_9:def 3 : (Bool "for" (Set (Var "f")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k3_euclid_9 :::"Intervals"::: ) "(" (Set (Var "f")) "," (Set (Var "r")) ")" )) "iff" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "r")) ")" ) "," (Set "(" (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "r")) ")" ) ($#k2_rcomp_1 :::".["::: ) )) ")" ) ")" ) ")" )))); registrationlet "r" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set ($#k3_euclid_9 :::"Intervals"::: ) "(" (Set ($#k1_xboole_0 :::"{}"::: ) ) "," "r" ")" ) -> ($#v1_xboole_0 :::"empty"::: ) ; end; registrationlet "f" be ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"FinSequence":::); let "r" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set ($#k3_euclid_9 :::"Intervals"::: ) "(" "f" "," "r" ")" ) -> ($#v1_finseq_1 :::"FinSequence-like"::: ) ; end; definitionlet "n" be ($#m1_hidden :::"Nat":::); let "e" be ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Set (Const "n")) ")" ); let "r" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; func :::"OpenHypercube"::: "(" "e" "," "r" ")" -> ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set "(" ($#k14_euclid :::"Euclid"::: ) "n" ")" ) ")" ) equals :: EUCLID_9:def 4 (Set ($#k4_card_3 :::"product"::: ) (Set "(" ($#k3_euclid_9 :::"Intervals"::: ) "(" "e" "," "r" ")" ")" )); end; :: deftheorem defines :::"OpenHypercube"::: EUCLID_9:def 4 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Set (Var "n")) ")" ) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k4_euclid_9 :::"OpenHypercube"::: ) "(" (Set (Var "e")) "," (Set (Var "r")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_card_3 :::"product"::: ) (Set "(" ($#k3_euclid_9 :::"Intervals"::: ) "(" (Set (Var "e")) "," (Set (Var "r")) ")" ")" )))))); theorem :: EUCLID_9:11 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r")))) "holds" (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set ($#k4_euclid_9 :::"OpenHypercube"::: ) "(" (Set (Var "e")) "," (Set (Var "r")) ")" ))))) ; registrationlet "n" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m1_hidden :::"Nat":::); let "e" be ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Set (Const "n")) ")" ); let "r" be ($#~v2_xxreal_0 "non" ($#v2_xxreal_0 :::"positive"::: ) ) ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set ($#k4_euclid_9 :::"OpenHypercube"::: ) "(" "e" "," "r" ")" ) -> ($#v1_xboole_0 :::"empty"::: ) ; end; theorem :: EUCLID_9:12 (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ) "holds" (Bool (Set ($#k4_euclid_9 :::"OpenHypercube"::: ) "(" (Set (Var "e")) "," (Set (Var "r")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) )))) ; registrationlet "e" be ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" ); let "r" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set ($#k4_euclid_9 :::"OpenHypercube"::: ) "(" "e" "," "r" ")" ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; registrationlet "n" be ($#m1_hidden :::"Nat":::); let "e" be ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Set (Const "n")) ")" ); let "r" be ($#v2_xxreal_0 :::"positive"::: ) ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set ($#k4_euclid_9 :::"OpenHypercube"::: ) "(" "e" "," "r" ")" ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: EUCLID_9:13 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "r")) "," (Set (Var "s")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "s")))) "holds" (Bool (Set ($#k4_euclid_9 :::"OpenHypercube"::: ) "(" (Set (Var "e")) "," (Set (Var "r")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k4_euclid_9 :::"OpenHypercube"::: ) "(" (Set (Var "e")) "," (Set (Var "s")) ")" ))))) ; theorem :: EUCLID_9:14 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "e1")) "," (Set (Var "e")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool "(" (Bool (Set (Var "n")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) "or" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) ")" ) & (Bool (Set (Var "e1")) ($#r2_hidden :::"in"::: ) (Set ($#k4_euclid_9 :::"OpenHypercube"::: ) "(" (Set (Var "e")) "," (Set (Var "r")) ")" ))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set "(" (Set "(" (Set (Var "e1")) ($#k8_rvsum_1 :::"-"::: ) (Set (Var "e")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set "(" (Set "(" (Set (Var "e1")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set (Var "e")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) ")" ))))) ; theorem :: EUCLID_9:15 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "e1")) "," (Set (Var "e")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "n")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "e1")) ($#r2_hidden :::"in"::: ) (Set ($#k4_euclid_9 :::"OpenHypercube"::: ) "(" (Set (Var "e")) "," (Set (Var "r")) ")" ))) "holds" (Bool (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set "(" ($#k12_rvsum_1 :::"sqr"::: ) (Set "(" (Set (Var "e1")) ($#k8_rvsum_1 :::"-"::: ) (Set (Var "e")) ")" ) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "n")) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "r")) ($#k3_square_1 :::"^2"::: ) ")" )))))) ; theorem :: EUCLID_9:16 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "e1")) "," (Set (Var "e")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "n")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "e1")) ($#r2_hidden :::"in"::: ) (Set ($#k4_euclid_9 :::"OpenHypercube"::: ) "(" (Set (Var "e")) "," (Set (Var "r")) ")" ))) "holds" (Bool (Set ($#k4_metric_1 :::"dist"::: ) "(" (Set (Var "e1")) "," (Set (Var "e")) ")" ) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "r")) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k6_square_1 :::"sqrt"::: ) (Set (Var "n")) ")" )))))) ; theorem :: EUCLID_9:17 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "n")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k4_euclid_9 :::"OpenHypercube"::: ) "(" (Set (Var "e")) "," (Set "(" (Set (Var "r")) ($#k13_complex1 :::"/"::: ) (Set "(" ($#k6_square_1 :::"sqrt"::: ) (Set (Var "n")) ")" ) ")" ) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "e")) "," (Set (Var "r")) ")" ))))) ; theorem :: EUCLID_9:18 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "n")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k4_euclid_9 :::"OpenHypercube"::: ) "(" (Set (Var "e")) "," (Set (Var "r")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "e")) "," (Set "(" (Set (Var "r")) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" ($#k6_square_1 :::"sqrt"::: ) (Set (Var "n")) ")" ) ")" ) ")" ))))) ; theorem :: EUCLID_9:19 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "e1")) "," (Set (Var "e")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "e1")) ($#r2_hidden :::"in"::: ) (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "e")) "," (Set (Var "r")) ")" ))) "holds" (Bool "ex" (Set (Var "m")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Set ($#k4_euclid_9 :::"OpenHypercube"::: ) "(" (Set (Var "e1")) "," (Set "(" (Num 1) ($#k13_complex1 :::"/"::: ) (Set (Var "m")) ")" ) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "e")) "," (Set (Var "r")) ")" )))))) ; theorem :: EUCLID_9:20 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "e1")) "," (Set (Var "e")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "n")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Var "e1")) ($#r2_hidden :::"in"::: ) (Set ($#k4_euclid_9 :::"OpenHypercube"::: ) "(" (Set (Var "e")) "," (Set (Var "r")) ")" ))) "holds" (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">"::: ) (Set (Set "(" ($#k3_euclid :::"abs"::: ) (Set "(" (Set (Var "e1")) ($#k8_rvsum_1 :::"-"::: ) (Set (Var "e")) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_euclid_9 :::"max_diff_index"::: ) "(" (Set (Var "e1")) "," (Set (Var "e")) ")" ")" )))))) ; theorem :: EUCLID_9:21 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "e1")) "," (Set (Var "e")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set ($#k4_euclid_9 :::"OpenHypercube"::: ) "(" (Set (Var "e1")) "," (Set "(" (Set (Var "r")) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set "(" ($#k3_euclid :::"abs"::: ) (Set "(" (Set (Var "e1")) ($#k8_rvsum_1 :::"-"::: ) (Set (Var "e")) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k1_euclid_9 :::"max_diff_index"::: ) "(" (Set (Var "e1")) "," (Set (Var "e")) ")" ")" ) ")" ) ")" ) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k4_euclid_9 :::"OpenHypercube"::: ) "(" (Set (Var "e")) "," (Set (Var "r")) ")" ))))) ; theorem :: EUCLID_9:22 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set ($#k9_metric_1 :::"Ball"::: ) "(" (Set (Var "e")) "," (Set (Var "r")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k4_euclid_9 :::"OpenHypercube"::: ) "(" (Set (Var "e")) "," (Set (Var "r")) ")" ))))) ; registrationlet "n" be ($#m1_hidden :::"Nat":::); let "e" be ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Set (Const "n")) ")" ); let "r" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set ($#k4_euclid_9 :::"OpenHypercube"::: ) "(" "e" "," "r" ")" ) -> ($#v3_pre_topc :::"open"::: ) ; end; theorem :: EUCLID_9:23 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set "(" ($#k14_euclid :::"Euclid"::: ) (Set (Var "n")) ")" ) ")" ) "st" (Bool (Bool (Set (Var "V")) "is" ($#v3_pre_topc :::"open"::: ) )) "holds" (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set (Var "V")))) "holds" (Bool "ex" (Set (Var "m")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Set ($#k4_euclid_9 :::"OpenHypercube"::: ) "(" (Set (Var "e")) "," (Set "(" (Num 1) ($#k13_complex1 :::"/"::: ) (Set (Var "m")) ")" ) ")" ) ($#r1_tarski :::"c="::: ) (Set (Var "V"))))))) ; theorem :: EUCLID_9:24 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "V")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set "(" ($#k14_euclid :::"Euclid"::: ) (Set (Var "n")) ")" ) ")" ) "st" (Bool (Bool "(" "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Set (Var "n")) ")" ) "st" (Bool (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set (Var "V")))) "holds" (Bool "ex" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool "(" (Bool (Set (Var "r")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set ($#k4_euclid_9 :::"OpenHypercube"::: ) "(" (Set (Var "e")) "," (Set (Var "r")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Var "V"))) ")" )) ")" )) "holds" (Bool (Set (Var "V")) "is" ($#v3_pre_topc :::"open"::: ) ))) ; definitionlet "n" be ($#m1_hidden :::"Nat":::); let "e" be ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Set (Const "n")) ")" ); func :::"OpenHypercubes"::: "e" -> ($#m1_subset_1 :::"Subset-Family":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set "(" ($#k14_euclid :::"Euclid"::: ) "n" ")" ) ")" ) equals :: EUCLID_9:def 5 "{" (Set "(" ($#k4_euclid_9 :::"OpenHypercube"::: ) "(" "e" "," (Set "(" (Num 1) ($#k13_complex1 :::"/"::: ) (Set (Var "m")) ")" ) ")" ")" ) where m "is" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool verum) "}" ; end; :: deftheorem defines :::"OpenHypercubes"::: EUCLID_9:def 5 : (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Set (Var "n")) ")" ) "holds" (Bool (Set ($#k5_euclid_9 :::"OpenHypercubes"::: ) (Set (Var "e"))) ($#r1_hidden :::"="::: ) "{" (Set "(" ($#k4_euclid_9 :::"OpenHypercube"::: ) "(" (Set (Var "e")) "," (Set "(" (Num 1) ($#k13_complex1 :::"/"::: ) (Set (Var "m")) ")" ) ")" ")" ) where m "is" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool verum) "}" ))); registrationlet "n" be ($#m1_hidden :::"Nat":::); let "e" be ($#m1_subset_1 :::"Point":::) "of" (Set "(" ($#k14_euclid :::"Euclid"::: ) (Set (Const "n")) ")" ); cluster (Set ($#k5_euclid_9 :::"OpenHypercubes"::: ) "e") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_tops_2 :::"open"::: ) (Set ($#k2_euclid_9 :::"@"::: ) "e") ($#v1_yellow_8 :::"-quasi_basis"::: ) ; end; theorem :: EUCLID_9:25 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")) ")" ) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_card_3 :::"product"::: ) (Set "(" ($#k12_pralg_1 :::"Carrier"::: ) (Set "(" (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")) ")" ) ($#k7_funcop_1 :::"-->"::: ) (Set ($#k3_topmetr :::"R^1"::: ) ) ")" ) ")" )))) ; theorem :: EUCLID_9:26 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "n")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "for" (Set (Var "PP")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set "(" ($#k14_euclid :::"Euclid"::: ) (Set (Var "n")) ")" ) ")" ) "st" (Bool (Bool (Set (Var "PP")) ($#r1_hidden :::"="::: ) (Set ($#k2_waybel18 :::"product_prebasis"::: ) (Set "(" (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")) ")" ) ($#k7_funcop_1 :::"-->"::: ) (Set ($#k3_topmetr :::"R^1"::: ) ) ")" )))) "holds" (Bool (Set (Var "PP")) "is" ($#v2_cantor_1 :::"quasi_prebasis"::: ) ))) ; theorem :: EUCLID_9:27 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "PP")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set "(" ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set "(" ($#k14_euclid :::"Euclid"::: ) (Set (Var "n")) ")" ) ")" ) "st" (Bool (Bool (Set (Var "PP")) ($#r1_hidden :::"="::: ) (Set ($#k2_waybel18 :::"product_prebasis"::: ) (Set "(" (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")) ")" ) ($#k7_funcop_1 :::"-->"::: ) (Set ($#k3_topmetr :::"R^1"::: ) ) ")" )))) "holds" (Bool (Set (Var "PP")) "is" ($#v1_tops_2 :::"open"::: ) ))) ; theorem :: EUCLID_9:28 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k3_pcomps_1 :::"TopSpaceMetr"::: ) (Set "(" ($#k14_euclid :::"Euclid"::: ) (Set (Var "n")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k3_waybel18 :::"product"::: ) (Set "(" (Set "(" ($#k2_finseq_1 :::"Seg"::: ) (Set (Var "n")) ")" ) ($#k7_funcop_1 :::"-->"::: ) (Set ($#k3_topmetr :::"R^1"::: ) ) ")" )))) ;