Quelle vect2_Heine.prf
Sprache: Lisp
(vect2_Heinenil 3476029646"" (rewrite "real_metric_space" ) nil nil )"set" sets nil ) (set type-eq-decl nil sets nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil real_metric_space "analysis/" ))nil ))nil 3476029646"" (rewrite "vect2_metric_space" ) nil nil )nil vect2_metric_space nil )) nil ))nil 3610811549"" (subtype-tcc) nil nil ) nil nil ))nil 3476029922"" (lemma "curried_min_exists" )"" (skosimp*)"" (inst - "closed_intv(A!1,B!1)" "fullset[Vect2]" "f!1" )"" (prop)"1" (inst - "y!1" )"1" (expand "fullset" )"1" (expand "nonempty?" )"1" (expand "empty?" )"1" (expand "member" ) (("1" (prop) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (inst - "y!1" )"2" (expand "fullset" ) (("2" (assert ) nil nil )) nil ))nil )"3" (inst - "y!1" )"3" (expand "fullset" ) (("3" (prop) nil nil )) nil )) nil )"4" (inst - "y!1" )"4" (expand "fullset" ) (("4" (prop) nil nil )) nil )) nil )"5" (expand "nonempty?" )"5" (expand "empty?" )"5" (copy -2)"5" (inst - "(A!1 + B!1)/2" )"5" (expand "member" ) (("5" (propax) nil nil ))nil ))nil ))nil ))nil ))nil )"6" (expand "nonempty?" )"6" (expand "empty?" )"6" (copy -2)"6" (inst - "(A!1 + B!1)/2" )"6" (expand "member" ) (("6" (propax) nil nil ))nil ))nil ))nil ))nil ))nil )"7" (expand "nonempty?" )"7" (expand "empty?" )"7" (inst - "(A!1 + B!1)/2" )"7" (expand "member" ) (("7" (propax) nil nil )) nil ))nil ))nil ))nil )"8" (expand "nonempty?" )"8" (expand "empty?" )"8" (expand "member" )"8" (inst - "(A!1 + B!1)/2" ) (("8" (assert ) nil nil ))nil ))nil ))nil ))nil )"9" (expand "nonempty?" )"9" (expand "empty?" )"9" (expand "member" )"9" (inst - "f!1(A!1,y!1)" )"9" (inst + "A!1" ) nil nil )) nil ))nil ))nil ))nil )"10" (expand "continuous?" )"10" (expand "continuous_at?" )"10" (skosimp*)"10" (inst - "x!1" )"1" (inst - "epsilon!1" )"1" (skosimp*)"1" (inst + "delta!1" )"1" (skosimp*)"1" (expand "member" )"1" (expand "ball" )"1" "y!2" )"1" (assert ) nil nil )"2" expand "extend" )"2" "1" expand "fullset" )"1" (propax) nil nil ))nil )"2" "y!2" )"2" expand "extend" )"2" (prop) nil nil ))nil ))nil )"3" "y!2" )"3" expand "extend" )"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "extend" )"2" (prop)"1" (expand "fullset" ) (("1" (propax) nil nil ))nil )"2" (typepred "x!1" )"2" (expand "extend" )"2" (assert ) nil nil )) nil ))nil )"3" (typepred "x!1" )"3" (expand "extend" )"3" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"11" (expand "continuous?" )"11" (expand "continuous_at?" )"11" (skosimp*)"11" (inst - "x!1" )"1" (inst - "epsilon!1" )"1" (skosimp*)"1" (inst + "delta!1" )"1" (skosimp*)"1" (expand "member" )"1" (expand "ball" )"1" "y!2" )"1" (assert ) nil nil )"2" expand "extend" )"2" "1" expand "fullset" )"1" (propax) nil nil ))nil )"2" "y!2" )"2" expand "extend" )"2" (assert ) nil nil ))nil ))nil )"3" "y!2" )"3" expand "extend" )"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "extend" )"2" (prop)"1" (expand "fullset" ) (("1" (propax) nil nil ))nil )"2" (typepred "x!1" )"2" (expand "extend" )"2" (assert ) nil nil )) nil ))nil )"3" (typepred "x!1" )"3" (expand "extend" )"3" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"12" (hide 1)"12" (expand "continuous?" )"12" (expand "continuous_at?" )"12" (skosimp*)"12" (inst - "x!1" )"1" (inst - "epsilon!1" )"1" (skosimp*)"1" (inst + "delta!1" )"1" (skosimp*)"1" (expand "member" )"1" expand "ball" )"1" "y!2" )"1" (assert ) nil nil )"2" expand "extend" )"2" "1" expand "fullset" )"1" (propax) nil nil ))nil )"2" "y!2" )"2" expand "extend" )"2" (prop) nil nil ))nil ))nil )"3" "y!2" )"3" expand "extend" )"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "extend" )"2" (prop)"1" (expand "fullset" )"1" (propax) nil nil )) nil )"2" (typepred "x!1" )"2" (expand "extend" )"2" (assert ) nil nil )) nil ))nil )"3" (typepred "x!1" )"3" (expand "extend" )"3" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"13" (expand "nonempty?" )"13" (expand "empty?" )"13" (expand "member" )"13" (inst - "f!1(A!1,y!1)" )"13" (inst + "A!1" ) nil nil )) nil ))nil ))nil ))nil )"14" (lemma "curried_min_exists" )"14" "closed_intv(A!1,B!1)" "fullset[Vect2]" "f!1" )"14" (assert )"14" (prop)"1" (inst - "y!1" )"1" (expand "fullset" ) (("1" (propax) nil nil ))nil ))nil )"2" (lemma "closed_intervals_compact" )"2" (inst - "A!1" "B!1" ) nil nil )) nil ))nil ))nil ))nil ))nil )"15" (lemma "closed_intervals_compact" )"15" (inst - "A!1" "B!1" ) nil nil )) nil )"16" (lemma "closed_intervals_compact" )"16" (inst - "A!1" "B!1" ) nil nil )) nil ))nil ))nil ))nil ))nil )"bool" sets nil )"bool" sets nil )"bool" sets nil )"real" reals nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"real" reals nil )"bool" continuity_ms_def "analysis/" )"real" vect2_Heine nil )"{x: real | A!1 < x}" vect2_Heine nil )"bool" booleans nil )"R" extend nil )"(extend LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect2])], bool,LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect2])]]))" nil )"set[T]" metric_spaces "analysis/" )NOT const-decl "[bool -> bool]" booleans nil )"(strict_total_order?[real])" real_props nil )"(extend LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect2])], bool,LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect2])]]))" nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" continuity_ms_def "analysis/" )"(extend LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect2])], bool,LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect2])]]))" nil )"(extend LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect2])], bool,LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect2])]]))" nil )"(extend LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect2])], bool,LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect2])]]))" nil )"(extend LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect2])], bool,LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect2])]]))" nil )nil real_metric_space"analysis/" )set type-eq-decl nil sets nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil ) (< const-decl "bool" reals nil )"set" sets nil )"(total_order?[real])" nil )nil cross_metric_real_fun"analysis/" )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )"bool" reals nil )nil real_types nil )"nnreal" real_metric_space "analysis/" )nil vectors_2D_def "vectors/" )"nnreal" distance_2D "vectors/" ))nil )nil 3476029872"" (lemma "curried_min_exists" )"" (skosimp*)"" (inst - "closed_intv(A!1,B!1)" "fullset[Vect2]" "f!1" )"" (prop)"1" (inst - "y!1" )"1" (expand "fullset" )"1" (expand "nonempty?" )"1" (expand "empty?" )"1" (expand "member" ) (("1" (prop) nil )))))))))))"2" (inst - "y!1" )"2" (expand "fullset" ) (("2" (prop) nil )))))"2" (inst - "y!1" )"2" (expand "fullset" ) (("2" (assert ) nil )))))"4" (inst - "y!1" )"4" (expand "fullset" ) (("4" (prop) nil )))))"5" (expand "nonempty?" )"5" (expand "empty?" )"5" (copy -2)"5" (inst - "(A!1 + B!1)/2" )"5" (expand "member" ) (("5" (propax) nil )))))))))))"6" (expand "nonempty?" )"6" (expand "empty?" )"6" (copy -2)"6" (inst - "(A!1 + B!1)/2" )"6" (expand "member" ) (("6" (propax) nil )))))))))))"7" (expand "nonempty?" )"7" (expand "empty?" )"7" (inst - "(A!1 + B!1)/2" )"7" (expand "member" ) (("7" (propax) nil )))))))))"8" (expand "nonempty?" )"8" (expand "empty?" )"8" (expand "member" )"8" (inst - "(A!1 + B!1)/2" )"8" (assert ) nil )))))))))"9" (expand "nonempty?" )"9" (expand "empty?" )"9" (expand "member" )"9" (inst - "f!1(A!1,y!1)" )"9" (inst + "A!1" ) nil )))))))))"10" (expand "continuous?" )"10" (expand "continuous_at?" )"10" (skosimp*)"10" (inst - "x!1" )"1" (inst - "epsilon!1" )"1" (skosimp*)"1" (inst + "delta!1" )"1" (skosimp*)"1" (expand "member" )"1" (expand "ball" )"1" "y!2" )"1" (assert ) nil )"2" expand "extend" )"2" "1" expand "fullset" )"1" (propax) nil )))"2" "y!2" )"2" expand "extend" )"2" (assert ) nil )))))"2" "y!2" )"2" expand "extend" )"2" nil )))))))))))))))))))))))"2" (expand "extend" )"2" (prop)"1" (expand "fullset" ) (("1" (propax) nil )))"2" (typepred "x!1" )"2" (expand "extend" ) (("2" (assert ) nil )))))"2" (typepred "x!1" )"2" (expand "extend" )"2" (assert ) nil )))))))))))))))))"11" (expand "continuous?" )"11" (expand "continuous_at?" )"11" (skosimp*)"11" (inst - "x!1" )"1" (inst - "epsilon!1" )"1" (skosimp*)"1" (inst + "delta!1" )"1" (skosimp*)"1" (expand "member" )"1" (expand "ball" )"1" "y!2" )"1" (assert ) nil )"2" expand "extend" )"2" "1" expand "fullset" )"1" (propax) nil )))"2" "y!2" )"2" expand "extend" )"2" (assert ) nil )))))"2" "y!2" )"2" expand "extend" )"2" assert )nil )))))))))))))))))))))))"2" (expand "extend" )"2" (prop)"1" (expand "fullset" ) (("1" (propax) nil )))"2" (typepred "x!1" )"2" (expand "extend" ) (("2" (assert ) nil )))))"2" (typepred "x!1" )"2" (expand "extend" )"2" (assert ) nil )))))))))))))))))"12" (expand "nonempty?" )"12" (expand "empty?" )"12" (expand "member" )"12" (inst - "f!1(A!1,y!1)" )"12" (inst + "A!1" ) nil )))))))))"12" (hide 1)"12" (expand "continuous?" )"12" (expand "continuous_at?" )"12" (skosimp*)"12" (inst - "x!1" )"1" (inst - "epsilon!1" )"1" (skosimp*)"1" (inst + "delta!1" )"1" (skosimp*)"1" (expand "member" )"1" expand "ball" )"1" "y!2" )"1" (assert ) nil )"2" expand "extend" )"2" "1" expand "fullset" )"1" (propax) nil )))"2" "y!2" )"2" expand "extend" )"2" (prop) nil )))))"2" "y!2" )"2" expand "extend" )"2" assert )nil )))))))))))))))))))))))"2" (expand "extend" )"2" (prop)"1" (expand "fullset" ) (("1" (propax) nil )))"2" (typepred "x!1" )"2" (expand "extend" )"2" (assert ) nil )))))"2" (typepred "x!1" )"2" (expand "extend" )"2" (assert ) nil )))))))))))))))))))"14" (lemma "curried_min_exists" )"14" "closed_intv(A!1,B!1)" "fullset[Vect2]" "f!1" )"14" (assert )"14" (prop)"1" (inst - "y!1" )"1" (expand "fullset" ) (("1" (propax) nil )))))"2" (lemma "closed_intervals_compact" )"2" (inst - "A!1" "B!1" ) nil )))))))))))"15" (lemma "closed_intervals_compact" )"15" (inst - "A!1" "B!1" ) nil )))"16" (lemma "closed_intervals_compact" )"16" (inst - "A!1" "B!1" ) nil ))))))))))nil )nil nil ))nil 3476029777"" (lemma "curried_min_exists" )"" (skosimp*)"" (inst - "closed_intv(A!1,B!1)" "fullset[Vect2]" "f!1" )"" (prop)"1" (inst - "y!1" )"1" (expand "fullset" )"1" (expand "nonempty?" )"1" (expand "empty?" )"1" (expand "member" ) (("1" (prop) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (inst - "y!1" )"2" (expand "fullset" ) (("2" (prop) nil nil )) nil )) nil )"3" (inst - "y!1" )"3" (expand "fullset" ) (("3" (assert ) nil nil )) nil ))nil )"4" (expand "nonempty?" )"4" (expand "empty?" )"4" (copy -2)"4" (inst - "(A!1 + B!1)/2" )"4" (expand "member" ) (("4" (propax) nil nil ))nil ))nil ))nil ))nil ))nil )"5" (expand "nonempty?" )"5" (expand "empty?" )"5" (copy -2)"5" (inst - "(A!1 + B!1)/2" )"5" (expand "member" ) (("5" (propax) nil nil ))nil ))nil ))nil ))nil ))nil )"6" (expand "nonempty?" )"6" (expand "empty?" )"6" (copy -2)"6" (inst - "(A!1 + B!1)/2" )"6" (expand "member" ) (("6" (propax) nil nil ))nil ))nil ))nil ))nil ))nil )"7" (expand "nonempty?" )"7" (expand "empty?" )"7" (expand "member" )"7" (inst - "f!1(A!1,y!1)" )"7" (inst + "A!1" ) nil nil )) nil ))nil ))nil ))nil )"8" (expand "continuous?" )"8" (expand "continuous_at?" )"8" (skosimp*)"8" (inst - "x!1" )"1" (inst - "epsilon!1" )"1" (skosimp*)"1" (inst + "delta!1" )"1" (skosimp*)"1" (expand "member" )"1" (expand "ball" )"1" "y!2" )"1" (assert ) nil nil )"2" expand "extend" )"2" "1" expand "fullset" )"1" (propax) nil nil ))nil )"2" "y!2" )"2" expand "extend" )"2" (assert ) nil nil ))nil ))nil )"3" "y!2" )"3" expand "extend" )"3" (prop) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "extend" )"2" (prop)"1" (expand "fullset" ) (("1" (propax) nil nil ))nil )"2" (typepred "x!1" )"2" (expand "extend" )"2" (assert ) nil nil )) nil ))nil )"3" (typepred "x!1" )"3" (expand "extend" )"3" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"9" (expand "continuous?" )"9" (expand "continuous_at?" )"9" (skosimp*)"9" (inst - "x!1" )"1" (inst - "epsilon!1" )"1" (skosimp*)"1" (inst + "delta!1" )"1" (skosimp*)"1" (expand "member" )"1" (expand "ball" )"1" "y!2" )"1" (assert ) nil nil )"2" expand "extend" )"2" "1" expand "fullset" )"1" (propax) nil nil ))nil )"2" "y!2" )"2" expand "extend" )"2" (assert ) nil nil ))nil ))nil )"3" "y!2" )"3" expand "extend" )"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "extend" )"2" (prop)"1" (expand "fullset" ) (("1" (propax) nil nil ))nil )"2" (typepred "x!1" )"2" (expand "extend" )"2" (assert ) nil nil )) nil ))nil )"3" (typepred "x!1" )"3" (expand "extend" )"3" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"10" (expand "nonempty?" )"10" (expand "empty?" )"10" (expand "member" )"10" (inst - "f!1(A!1,y!1)" )"10" (inst + "A!1" ) nil nil )) nil ))nil ))nil ))nil )"11" (lemma "curried_min_exists" )"11" "closed_intv(A!1,B!1)" "fullset[Vect2]" "f!1" )"11" (assert )"11" (prop)"1" (inst - "y!1" )"1" (expand "fullset" ) (("1" (propax) nil nil ))nil ))nil )"2" (lemma "closed_intervals_compact" )"2" (inst - "A!1" "B!1" ) nil nil )) nil ))nil ))nil ))nil ))nil )"12" (lemma "closed_intervals_compact" )"12" (inst - "A!1" "B!1" ) nil nil )) nil ))nil ))nil ))nil ))nil )"bool" sets nil )"bool" sets nil )"bool" sets nil )"real" reals nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"real" reals nil )"bool" continuity_ms_def "analysis/" )"real" vect2_Heine nil )"{x: real | A!1 < x}" vect2_Heine nil )"bool" booleans nil )"R" extend nil )"(extend LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect2])], bool,LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect2])]]))" nil )"set[T]" metric_spaces "analysis/" )NOT const-decl "[bool -> bool]" booleans nil )"(strict_total_order?[real])" real_props nil )"(extend LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect2])], bool,LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect2])]]))" nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" continuity_ms_def "analysis/" )"(extend LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect2])], bool,LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect2])]]))" nil )"(extend LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect2])], bool,LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect2])]]))" nil )nil real_metric_space"analysis/" )set type-eq-decl nil sets nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil ) (< const-decl "bool" reals nil )"set" sets nil )"(total_order?[real])" nil )nil cross_metric_real_fun"analysis/" )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )"bool" reals nil )nil real_types nil )"nnreal" real_metric_space "analysis/" )nil vectors_2D_def "vectors/" )"nnreal" distance_2D "vectors/" ))nil )nil 3476029646"" (subtype-tcc) nil nil ) nil nil ))nil 3476030045"" (skosimp*)"" (lemma "curried_min_is_cont" )"" (inst - "closed_intv(A!1,B!1)" "fullset[Vect2]" "f!1" )"" (prop)"1" (expand "continuous?" +)"1" (expand "fullset" ) (("1" (propax) nil nil )) nil ))nil )"2" (lemma "closed_intervals_compact" )"2" (inst?) nil nil )) nil )"3" (hide 2)"3" (expand "continuous?" )"3" (skosimp*)"3" (inst - "x!1" )"1" (expand "continuous_at?" )"1" (skosimp*)"1" (inst - "epsilon!1" )"1" (skosimp*)"1" (inst + "delta !1" )"1" (skosimp*)"1" expand "member" )"1" expand "ball" )"1" "y!1" )"1" "y!1" )"1" (assert ) nil nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (typepred "x!1" ) (("2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" (expand "nonempty?" )"4" (expand "empty?" )"4" (expand "member" )"4" (inst - "(A!1 + B!1)/2" ) (("4" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"nnreal" distance_2D "vectors/" )nil vectors_2D_def "vectors/" )"nnreal" real_metric_space "analysis/" )nil real_types nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil cross_metric_real_fun"analysis/" )"bool" continuity_ms_def "analysis/" )nil real_metric_space"analysis/" )"bool" continuity_ms_def "analysis/" )"real" vect2_Heine nil )"{x: real | A!1 < x}" vect2_Heine nil )"bool" booleans nil )"R" extend nil )"(extend LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect2])], bool,LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect2])]]))" nil )"set[T]" metric_spaces "analysis/" )"(extend LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect2])], bool,LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect2])]]))" nil )"(strict_total_order?[real])" real_props nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" sets nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" continuity_ms_def "analysis/" )"bool" sets nil )"real" reals nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"real" reals nil )"bool" sets nil )set type-eq-decl nil sets nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil ) (< const-decl "bool" reals nil )"set" sets nil )"(total_order?[real])" nil ))nil ))nil 3476029826"" (lemma "curried_min_is_cont_2D_TCC1" )"" (skosimp*)"" (inst - "f!1" "A!1" "B!1" )"" (prop)"1" (inst - "y1!1" ) (("1" (prop) nil nil )) nil )"2" (inst - "y1!1" ) (("2" (prop) nil nil )) nil )"3" (inst - "y1!1" ) (("3" (prop) nil nil )) nil )"4" (lemma "product_cont_product_subset" )"4" "closed_intv(A!1,B!1)" "fullset[Vect2]" "f!1" )"4" (prop)"1" (hide-all-but (-1 2))"1" (expand "continuous?" )"1" (expand "continuous_at?" )"1" (expand "member" )"1" (expand "ball" )"1" (skosimp*)"1" (inst - "x!1" )"1" "epsilon!1" )"1" "1" "delta!1" )"1" "1" "y!1" )"1" (assert ) nil nil )"2" expand "extend" )"2" "1" expand "fullset" )"1" (propax) nil nil ))nil )"2" "y!1" )"2" expand "extend" )"2" assert )nil nil ))nil ))nil )"3" "y!1" )"3" expand "extend" )"3" assert )nil nil ))nil ))nil )"4" expand "fullset" )"4" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "extend" )"2" "1" expand "fullset" )"1" (propax) nil nil ))nil )"2" "x!1" )"2" expand "extend" )"2" (assert ) nil nil ))nil ))nil )"3" "x!1" )"3" expand "extend" )"3" (assert ) nil nil ))nil ))nil )"4" expand "fullset" )"4" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but (-1 1))"2" (skosimp*)"2" (inst - "x!1" "y!1" "epsilon!1" )"2" (skosimp*)"2" (inst + "delta!1" )"2" (skosimp*)"2" (inst - "z!1" "w!1" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"5" (hide 1)"5" (lemma "product_cont_product_subset" )"5" "closed_intv(A!1,B!1)" "fullset[Vect2]" "f!1" )"5" (prop)"1" (hide-all-but (-1 1))"1" (expand "continuous?" )"1" (expand "continuous_at?" )"1" (expand "member" )"1" (expand "ball" )"1" (skosimp*)"1" "x!1" )"1" "epsilon!1" )"1" "1" "delta!1" )"1" "1" "y!1" )"1" (assert ) nil nil )"2" expand "extend" )"2" "1" expand "fullset" )"1" nil nil ))nil )"2" "y!1" )"2" expand "extend" )"2" assert )nil nil ))nil ))nil )"3" "y!1" )"3" expand "extend" )"3" assert )nil nil ))nil ))nil )"4" expand "fullset" )"4" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "extend" )"2" "1" expand "fullset" )"1" (propax) nil nil ))nil )"2" "x!1" )"2" expand "extend" )"2" (assert ) nil nil ))nil ))nil )"3" "x!1" )"3" expand "extend" )"3" (assert ) nil nil ))nil ))nil )"4" expand "fullset" )"4" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but (-1 1))"2" (skosimp*)"2" (inst - "x!1" "y!1" "epsilon!1" )"2" (skosimp*)"2" (inst + "delta!1" )"2" (skosimp*)"2" "z!1" "w!1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"6" (hide 1)"6" (lemma "product_cont_product_subset" )"6" "closed_intv(A!1,B!1)" "fullset[Vect2]" "f!1" )"6" (prop)"1" (hide-all-but (-1 1))"1" (expand "continuous?" )"1" (expand "continuous_at?" )"1" (expand "member" )"1" (expand "ball" )"1" (skosimp*)"1" "x!1" )"1" "epsilon!1" )"1" "1" "delta!1" )"1" "1" "y!1" )"1" (assert ) nil nil )"2" expand "extend" )"2" "1" expand "fullset" )"1" nil nil ))nil )"2" "y!1" )"2" expand "extend" )"2" assert )nil nil ))nil ))nil )"3" "y!1" )"3" expand "extend" )"3" assert )nil nil ))nil ))nil )"4" expand "fullset" )"4" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "extend" )"2" "1" expand "fullset" )"1" (propax) nil nil ))nil )"2" "x!1" )"2" expand "extend" )"2" (assert ) nil nil ))nil ))nil )"3" "x!1" )"3" expand "extend" )"3" (assert ) nil nil ))nil ))nil )"4" expand "fullset" )"4" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but (-1 1))"2" (skosimp*)"2" (inst - "x!1" "y!1" "epsilon!1" )"2" (skosimp*)"2" (inst + "delta!1" )"2" (skosimp*)"2" "z!1" "w!1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"(total_order?[real])" nil )"set" sets nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )set type-eq-decl nil sets nil )"bool" continuity_ms_def "analysis/" )"set[T]" metric_spaces "analysis/" )"real" vect2_Heine nil )"{x: real | A!1 < x}" vect2_Heine nil )"bool" booleans nil )"R" extend nil )"(extend LAMBDA (x: real): A!1 <= x AND x <= B!1), Vect2],LAMBDA (x: real): A!1 <= x AND x <= B!1), Vect2]]))" nil )NOT const-decl "[bool -> bool]" booleans nil )"(strict_total_order?[real])" real_props nil )"(extend LAMBDA (x: real): A!1 <= x AND x <= B!1), Vect2],LAMBDA (x: real): A!1 <= x AND x <= B!1), Vect2]]))" nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" sets nil )"bool" continuity_ms_def "analysis/" )nil cross_metric_cont"analysis/" )"bool" reals nil )nil real_types nil )"nnreal" real_metric_space "analysis/" )"nnreal" distance_2D "vectors/" )"(extend LAMBDA (x: real): A!1 <= x AND x <= B!1), Vect2],LAMBDA (x: real): A!1 <= x AND x <= B!1), Vect2]]))" nil )"(extend LAMBDA (x: real): A!1 <= x AND x <= B!1), Vect2],LAMBDA (x: real): A!1 <= x AND x <= B!1), Vect2]]))" nil )"(extend LAMBDA (x: real): A!1 <= x AND x <= B!1), Vect2],LAMBDA (x: real): A!1 <= x AND x <= B!1), Vect2]]))" nil )"(extend LAMBDA (x: real): A!1 <= x AND x <= B!1), Vect2],LAMBDA (x: real): A!1 <= x AND x <= B!1), Vect2]]))" nil )"bool" reals nil )nil booleans nil )nil vectors_2D_def "vectors/" )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil vect2_Heine nil ))nil )nil 3476029646"" (subtype-tcc) nil nil ) nil nil ))nil 3476030194"" (skosimp*)"" (skoletin 1)"1" (skosimp*)"1" (lemma "curried_min_is_cont_2D" )"1" (inst - "f!1" "A!1" "B!1" )"1" (prop)"1" (assert )"1" (replace -2 - rl)"1" (expand "continuous?" )"1" (expand "continuous?" )"1" (inst - "y!1" )"1" (expand "continuous_at?" )"1" (inst - "epsilon!1" )"1" (expand "member" )"1" expand "ball" )"1" "1" "delta!1" )"1" "1" "q!1" )"1" (assert ) nil nil )"2" expand "fullset" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "fullset" )"2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (lemma "product_cont_product_subset" )"2" "closed_intv(A!1,B!1)" "fullset[Vect2]" "f!1" )"2" (prop)"1" (hide-all-but (-1 1))"1" (expand "continuous?" )"1" (expand "continuous_at?" )"1" (expand "member" )"1" expand "ball" )"1" "1" "x!1" )"1" "epsilon!2" )"1" "1" "delta!1" )"1" "1" "y!2" )"1" (assert ) nil nil )"2" expand "extend" )"2" "1" expand "fullset" )"1" nil nil ))nil )"2" "y!2" )"2" expand "extend" )"2" assert )nil nil ))nil ))nil )"3" "y!2" )"3" expand "extend" )"3" assert )nil nil ))nil ))nil )"4" expand "fullset" )"4" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "extend" )"2" "1" expand "fullset" )"1" (propax) nil nil ))nil )"2" "x!1" )"2" expand "extend" )"2" (assert ) nil nil ))nil ))nil )"3" "x!1" )"3" expand "extend" )"3" (assert ) nil nil ))nil ))nil )"4" expand "fullset" )"4" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (inst - "x!1" "y!2" "epsilon!2" )"2" (skosimp*)"2" (inst + "delta!1" )"2" "2" "z!1" "w!1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (hide -)"2" (lemma "curried_min_is_cont_TCC1" )"2" (skosimp*)"2" "closed_intv(A!1,B!1)" "fullset[Vect2]" "f!1" )"2" case "nonempty?(LAMBDA (x: real): A!1 <= x AND x <= B!1)" )"1" (assert )"1" (reveal -2)"1" (label "cont_ed" -1)"1" (label "nonempty" -2)"1" (label "bigpred" -3)"1" (prop)"1" "y!1" )"1" expand "fullset" )"1" (assert ) nil nil ))nil ))nil )"2" "y!1" )"2" expand "fullset" )"2" (assert ) nil nil ))nil ))nil )"3" "y!1" )"3" expand "fullset" )"3" (assert ) nil nil ))nil ))nil )"4" expand "nonempty?" )"4" expand "empty?" )"4" expand "member" )"4" "f!1(A!1,y!1)" )"4" (inst + "A!1" ) nil nil ))nil ))nil ))nil ))nil )"5" "product_cont_product_subset" )"5" "closed_intv(A!1,B!1)" "fullset[Vect2]" "f!1" )"5" assert )"5" "cont_ed" 1))"5" "5" "x!1" "y!2" "epsilon!1" )"5" "5" "delta!1" )"5" "5" "z!1" "w!1" )"5" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"6" "product_cont_product_subset" )"6" "closed_intv(A!1,B!1)" "fullset[Vect2]" "f!1" )"6" assert )"6" "cont_ed" 1))"6" "6" "x!1" "y!2" "epsilon!1" )"6" "6" "delta!1" )"6" "6" "z!1" "w!1" )"6" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"7" expand "nonempty?" )"7" expand "empty?" )"7" expand "member" )"7" "f!1(A!1,y!1)" )"7" (inst + "A!1" ) nil nil ))nil ))nil ))nil ))nil )"8" "closed_intervals_compact" )"8" (inst - "A!1" "B!1" ) nil nil ))nil )"9" "closed_intervals_compact" )"9" (inst - "A!1" "B!1" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "nonempty?" )"2" (expand "empty?" )"2" (expand "member" )"2" (inst - "A!1" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil booleans nil )nil booleans nil )"bool" functions nil )"(bijective?[T, T])" identity nil )"bool" booleans nil )nil reals nil )nil vectors_2D_def "vectors/" )AND const-decl "[bool, bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )set type-eq-decl nil sets nil )"bool" sets nil )"bool" reals nil ) (< const-decl "bool" reals nil )"[T, T -> boolean]" equalities nil )nil defined_types nil )"bool" bounded_reals "reals/" )nil bounded_reals "reals/" )ext const-decl "set[real]" bounded_reals "reals/" )nil defined_types nil )"bool" bound_defs "reals/" )"{x | greatest_lower_bound(<=)(x, Sl)}" "reals/" )"[bool, bool -> bool]" booleans nil )min const-decl "T" bounded_reals "reals/" )nil bounded_reals "reals/" )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"[bool, bool -> bool]" booleans nil )nil real_types nil )"nnreal" distance_2D "vectors/" )"nnreal" real_metric_space "analysis/" )nil vect2_Heine nil )"bool" continuity_ms_def "analysis/" )"bool" continuity_ms_def "analysis/" )"bool" sets nil )"(strict_total_order?[real])" real_props nil )"Vect2" vect2_Heine nil )"set[T]" metric_spaces "analysis/" )"Vect2" vect2_Heine nil )"set" sets nil )"bool" continuity_ms_def "analysis/" )nil cross_metric_cont"analysis/" )"(extend LAMBDA (x: real): A!1 <= x AND x <= B!1), Vect2],LAMBDA (x: real): A!1 <= x AND x <= B!1), Vect2]]))" nil )NOT const-decl "[bool -> bool]" booleans nil )"(extend LAMBDA (x: real): A!1 <= x AND x <= B!1), Vect2],LAMBDA (x: real): A!1 <= x AND x <= B!1), Vect2]]))" nil )"R" extend nil )"bool" booleans nil )"{x: real | A!1 < x}" vect2_Heine nil )"real" vect2_Heine nil )"(total_order?[real])" nil ))nil )nil 3476030154"" (skosimp*)"" (skoletin 1)"1" (skosimp*)"1" (lemma "curried_min_is_cont_3D" )"1" (inst - "f!1" "A!1" "B!1" )"1" (prop)"1" (assert )"1" (replace -2 - rl)"1" (expand "continuous?" )"1" (expand "continuous?" )"1" (inst - "y!1" )"1" (expand "continuous_at?" )"1" (inst - "epsilon!1" )"1" (expand "member" )"1" expand "ball" )"1" "1" "delta!1" )"1" "1" "q!1" )"1" (assert ) nil )"2" expand "fullset" )"2" nil )))))))))))))))))))"2" (expand "fullset" )"2" (propax) nil )))))))))))))"2" (hide 2)"2" (lemma "product_cont_product_subset" )"2" "closed_intv(A!1,B!1)" "fullset[Vect2]" "f!1" )"2" (prop)"1" (hide-all-but (-1 1))"1" (expand "continuous?" )"1" (expand "continuous_at?" )"1" (expand "member" )"1" expand "ball" )"1" "1" "x!1" )"1" "epsilon!2" )"1" "1" "delta!1" )"1" "1" "y!2" )"1" (assert ) nil )"2" expand "extend" )"2" "1" expand "fullset" )"1" nil )))"2" "y!2" )"2" expand "extend" )"2" assert )nil )))))"3" "y!2" )"3" expand "extend" )"3" assert )nil )))))"4" expand "fullset" )"4" nil )))))))))))))))))"2" expand "extend" )"2" "1" expand "fullset" )"1" (propax) nil )))"2" "x!1" )"2" expand "extend" )"2" (assert ) nil )))))"3" "x!1" )"3" expand "extend" )"3" (assert ) nil )))))"4" expand "fullset" )"4" nil )))))))))))))))))))))"2" (skosimp*)"2" (inst - "x!1" "y!2" "epsilon!2" )"2" (skosimp*)"2" (inst + "delta!1" )"2" "2" "z!1" "w!1" )"2" assert )nil )))))))))))))))))))))))))))))"2" (hide 2)"2" (hide -)"2" (lemma "curried_min_is_cont_TCC1" )"2" (skosimp*)"2" "closed_intv(A!1,B!1)" "fullset[Vect2]" "f!1" )"2" case "nonempty?(LAMBDA (x: real): A!1 <= x AND x <= B!1)" )"1" (assert )"1" (reveal -2)"1" (label "cont_ed" -1)"1" (label "nonempty" -2)"1" (label "bigpred" -3)"1" (prop)"1" "y!1" )"1" expand "fullset" )"1" (assert ) nil )))))"2" "y!1" )"2" expand "fullset" )"2" (assert ) nil )))))"3" "y!1" )"3" expand "fullset" )"3" (assert ) nil )))))"4" expand "nonempty?" )"4" expand "empty?" )"4" expand "member" )"4" "f!1(A!1,y!1)" )"4" (inst + "A!1" ) nil )))))))))"5" "product_cont_product_subset" )"5" "closed_intv(A!1,B!1)" "fullset[Vect2]" "f!1" )"5" assert )"5" "cont_ed" 1))"5" "5" "x!1" "y!2" "epsilon!1" )"5" "5" "delta!1" )"5" "5" "z!1" "w!1" )"5" assert )nil )))))))))))))))))))))"6" "product_cont_product_subset" )"6" "closed_intv(A!1,B!1)" "fullset[Vect2]" "f!1" )"6" assert )"6" "cont_ed" 1))"6" "6" "x!1" "y!2" "epsilon!1" )"6" "6" "delta!1" )"6" "6" "z!1" "w!1" )"6" assert )nil )))))))))))))))))))))"7" expand "nonempty?" )"7" expand "empty?" )"7" expand "member" )"7" "f!1(A!1,y!1)" )"7" (inst + "A!1" ) nil )))))))))"8" "closed_intervals_compact" )"8" (inst - "A!1" "B!1" ) nil )))"9" "closed_intervals_compact" )"9" "A!1" "B!1" )nil )))))))))))))))"2" (expand "nonempty?" )"2" (expand "empty?" )"2" (expand "member" )"2" (inst - "A!1" )"2" (assert ) nil ))))))))))))))))))))))))nil )nil nil )nil 3476030132"" (skosimp*)"" (skoletin 1)"1" (skosimp*)"1" (lemma "curried_min_is_cont_3D" )"1" (inst - "f!1" "A!1" "B!1" )"1" (prop)"1" (assert )"1" (replace -2 - rl)"1" (expand "continuous?" )"1" (expand "continuous?" )"1" (inst - "y!1" )"1" (expand "continuous_at?" )"1" (inst - "epsilon!1" )"1" (expand "member" )"1" expand "ball" )"1" "1" "delta!1" )"1" "1" "q!1" )"1" (assert ) nil )"2" expand "fullset" )"2" nil )))))))))))))))))))"2" (expand "fullset" )"2" (propax) nil )))))))))))))"2" (hide 2)"2" (lemma "product_cont_product_subset" )"2" "closed_intv(A!1,B!1)" "fullset[Vect2]" "f!1" )"2" (prop)"1" (hide-all-but (-1 1))"1" (expand "continuous?" )"1" (expand "continuous_at?" )"1" (expand "member" )"1" expand "ball" )"1" "1" "x!1" )"1" "epsilon!2" )"1" "1" "delta!1" )"1" "1" "y!2" )"1" (assert ) nil )"2" expand "extend" )"2" "1" expand "fullset" )"1" nil )))"2" "y!2" )"2" expand "extend" )"2" assert )nil )))))"3" "y!2" )"3" expand "extend" )"3" assert )nil )))))"4" expand "fullset" )"4" nil )))))))))))))))))"2" expand "extend" )"2" "1" expand "fullset" )"1" (propax) nil )))"2" "x!1" )"2" expand "extend" )"2" (assert ) nil )))))"3" "x!1" )"3" expand "extend" )"3" (assert ) nil )))))"4" expand "fullset" )"4" nil )))))))))))))))))))))"2" (skosimp*)"2" (inst - "x!1" "y!2" "epsilon!2" )"2" (skosimp*)"2" (inst + "delta!1" )"2" "2" "z!1" "w!1" )"2" assert )nil )))))))))))))))))))))))))))))"2" (hide 2)"2" (hide -)"2" (lemma "curried_min_is_cont_TCC1" )"2" (skosimp*)"2" "closed_intv(A!1,B!1)" "fullset[Vect2]" "f!1" )"2" case "nonempty?(LAMBDA (x: real): A!1 <= x AND x <= B!1)" )"1" (assert )"1" (reveal -2)"1" (label "cont_ed" -1)"1" (label "nonempty" -2)"1" (label "bigpred" -3)"1" (prop)"1" "y!1" )"1" expand "fullset" )"1" (assert ) nil )))))"2" "y!1" )"2" expand "fullset" )"2" (assert ) nil )))))"3" "y!1" )"3" expand "fullset" )"3" (assert ) nil )))))"4" expand "nonempty?" )"4" expand "empty?" )"4" expand "member" )"4" "f!1(A!1,y!1)" )"4" (inst + "A!1" ) nil )))))))))"5" "product_cont_product_subset" )"5" "closed_intv(A!1,B!1)" "fullset[Vect2]" "f!1" )"5" assert )"5" "cont_ed" 1))"5" "5" "x!1" "y!2" "epsilon!1" )"5" "5" "delta!1" )"5" "5" "z!1" "w!1" )"5" assert )nil )))))))))))))))))))))"6" "product_cont_product_subset" )"6" "closed_intv(A!1,B!1)" "fullset[Vect2]" "f!1" )"6" assert )"6" "cont_ed" 1))"6" "6" "x!1" "y!2" "epsilon!1" )"6" "6" "delta!1" )"6" "6" "z!1" "w!1" )"6" assert )nil )))))))))))))))))))))"7" expand "nonempty?" )"7" expand "empty?" )"7" expand "member" )"7" "f!1(A!1,y!1)" )"7" (inst + "A!1" ) nil )))))))))"8" "closed_intervals_compact" )"8" (inst - "A!1" "B!1" ) nil )))"9" "closed_intervals_compact" )"9" "A!1" "B!1" )nil )))))))))))))))"2" (expand "nonempty?" )"2" (expand "empty?" )"2" (expand "member" )"2" (inst - "A!1" )"2" (assert ) nil ))))))))))))))))))))))))nil )nil nil ))nil 3476030244"" (skosimp*)"" (lemma "multiary_Heine" )"" (inst - "closed_intv(A!1,B!1)" "fullset[Vect2]" "f!1" )"" (assert )"" (prop)"1" (lemma "closed_intervals_compact" )"1" (inst - "A!1" "B!1" ) nil nil )) nil )"2" (expand "continuous?" )"2" (skosimp*)"2" (inst - "x!1" )"1" (expand "continuous_at?" )"1" (expand "member" )"1" (expand "ball" )"1" (skosimp*)"1" (inst - "epsilon!1" )"1" (skosimp*)"1" "delta!1" )"1" "1" "y!1" )"1" (assert ) nil nil )"2" expand "extend" )"2" "1" expand "fullset" )"1" (propax) nil nil ))nil )"2" "y!1" )"2" expand "extend" )"2" (assert ) nil nil ))nil ))nil )"3" "y!1" )"3" expand "extend" )"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "extend" )"2" (prop)"1" (expand "fullset" ) (("1" (propax) nil nil ))nil )"2" (typepred "x!1" )"2" (expand "extend" )"2" (assert ) nil nil )) nil ))nil )"3" (typepred "x!1" )"3" (expand "extend" )"3" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"nnreal" distance_2D "vectors/" )nil vectors_2D_def "vectors/" )"nnreal" real_metric_space "analysis/" )nil real_types nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil cross_metric_uniform_continuity"analysis/" )"bool" continuity_ms_def "analysis/" )"real" vect2_Heine nil )"{x: real | A!1 < x}" vect2_Heine nil )"bool" booleans nil )"R" extend nil )"(extend LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect2])], bool,LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect2])]]))" nil )"bool" sets nil )NOT const-decl "[bool -> bool]" booleans nil )"(strict_total_order?[real])" real_props nil )"(extend LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect2])], bool,LAMBDA (x: real): A!1 <= x AND x <= B!1), (fullset[Vect2])]]))" nil )nil real_types nil )"bool" reals nil )nil real_types nil )"set[T]" metric_spaces "analysis/" )"bool" continuity_ms_def "analysis/" )nil real_metric_space"analysis/" )set type-eq-decl nil sets nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil ) (< const-decl "bool" reals nil )"set" sets nil )"(total_order?[real])" nil ))nil ))nil 3476030277"" (skosimp*)"" (lemma "multiary_Heine_2D" )"" (inst - "f!1" "A!1" "B!1" )"" (expand "uniformly_continuous_in_first?" )"" (prop)"1" (inst - "y1!1" "epsilon!1" )"1" (skosimp*)"1" (inst + "delta!1" )"1" (skosimp*)"1" (inst - "x1!1" "x2!1" "y2!1" )"1" (assert ) nil nil )"2" (expand "fullset" ) (("2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "fullset" ) (("2" (propax) nil nil )) nil ))nil )"2" (lemma "product_cont_product_subset" )"2" "closed_intv(A!1,B!1)" "fullset[Vect2]" "f!1" )"2" (prop)"1" (hide-all-but (-1 1))"1" (expand "continuous?" )"1" (expand "continuous_at?" )"1" (expand "member" )"1" (expand "ball" )"1" (skosimp*)"1" "x!1" )"1" "epsilon!2" )"1" "1" "delta!1" )"1" "1" "y!1" )"1" (assert ) nil nil )"2" expand "extend" )"2" "1" expand "fullset" )"1" nil nil ))nil )"2" "y!1" )"2" expand "extend" )"2" assert )nil nil ))nil ))nil )"3" "y!1" )"3" expand "extend" )"3" assert )nil nil ))nil ))nil )"4" expand "fullset" )"4" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "extend" )"2" "1" expand "fullset" )"1" (propax) nil nil ))nil )"2" "x!1" )"2" expand "extend" )"2" (assert ) nil nil ))nil ))nil )"3" "x!1" )"3" expand "extend" )"3" (assert ) nil nil ))nil ))nil )"4" expand "fullset" )"4" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (inst - "x!1" "y!1" "epsilon!2" )"2" (skosimp*)"2" (inst + "delta!1" )"2" (skosimp*)"2" (inst - "z!1" "w!1" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil vect2_Heine nil )"bool" cross_metric_cont"analysis/" )"nnreal" distance_2D "vectors/" )"nnreal" real_metric_space "analysis/" )nil real_types nil )nil cross_metric_cont"analysis/" )"bool" continuity_ms_def "analysis/" )"bool" sets nil )"(extend LAMBDA (x: real): A!1 <= x AND x <= B!1), Vect2],LAMBDA (x: real): A!1 <= x AND x <= B!1), Vect2]]))" nil )NOT const-decl "[bool -> bool]" booleans nil )"(extend LAMBDA (x: real): A!1 <= x AND x <= B!1), Vect2],LAMBDA (x: real): A!1 <= x AND x <= B!1), Vect2]]))" nil )"R" extend nil )"bool" booleans nil )"{x: real | A!1 < x}" vect2_Heine nil )"real" vect2_Heine nil )"set[T]" metric_spaces "analysis/" )"bool" continuity_ms_def "analysis/" )set type-eq-decl nil sets nil ) (fullset const-decl "set" sets nil )"Vect2" vect2_Heine nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"Vect2" vect2_Heine nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"bool" reals nil )nil booleans nil )nil vectors_2D_def "vectors/" )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil ))nil )))
Messung V0.5 in Prozent C=100 H=96 G=97
¤ Dauer der Verarbeitung: 0.100 Sekunden
(vorverarbeitet am 2026-04-26)
¤ *© Formatika GbR, Deutschland
2026-05-26
