Quellcode-Bibliothek pointwise_convergence.prf
Sprache: Lisp
(pointwise_convergencenil 3391993987"" (skosimp)"" (expand "pointwise_bounded?" )"" (expand "pointwise_bounded_above?" )"" (expand "pointwise_bounded_below?" )"" (expand "pointwise?" )"" (split)"1" (flatten)"1" (split)"1" (skosimp)"1" (inst - "x!1" )"1" (rewrite "bounded_seq_def" )"1" (flatten) nil nil )) nil ))nil ))nil )"2" (skosimp)"2" (inst - "x!1" )"2" (rewrite "bounded_seq_def" )"2" (flatten) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (inst - "x!1" )"2" (inst - "x!1" )"2" (rewrite "bounded_seq_def" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" pointwise_convergence nil )"bool" pointwise_convergencenil )nil pointwise_convergence nil )nil sequences nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil convergence_aux "metric_space/" )"bool" pointwise_convergence nil )"bool" pointwise_convergencenil ))nil 3391989427"" (expand "zero_seq" )"" (expand "pointwise_bounded_above?" )"" (expand "bounded_above?" )"" (expand "pointwise?" )"" (expand "bounded_above?" )"" (expand "fullset" )"" (expand "image" )"" (expand "upper_bound?" )"" (skosimp*)"" (inst + "0" ) (("" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" pointwise_convergencenil )"bool" pointwise_convergence nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" real_fun_preds "reals/" )"real" pointwise_convergence nil ))nil ))nil 3391989427"" (expand "pointwise_bounded_below?" )"" (expand "pointwise?" )"" (expand "bounded_below?" )"" (expand "bounded_below?" )"" (skosimp) (("" (inst + "0" ) (("" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"bool" pointwise_convergence nil )"real" pointwise_convergence nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"bool" real_fun_preds "reals/" )"bool" pointwise_convergencenil ))nil ))nil 3391989427"" (expand "pointwise_bounded?" )"" (expand "pointwise?" )"" (expand "bounded_seq?" )"" (expand "bounded?" )"" (skosimp)"" (inst + "0" "1" ) (("" (grind) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )"bool" pointwise_convergence nil )"bool" metric_space_def "metric_space/" )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 )"bool" reals nil )nil real_types nil )NOT const-decl "[bool -> bool]" booleans nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"(strict_total_order?[real])" real_props nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )set type-eq-decl nil sets nil ) (fullset const-decl "set" sets nil )"real" pointwise_convergence nil )"set[R]" function_image nil )"bool" sets nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )"set[T]" metric_space_def "metric_space/" )"bool" sets nil )"(partial_order?[set[T]])" nil )"metric_open[real, (LAMBDA (x, y: real): abs(x - y))]" "metric_space/" )"real" reals nil )"real" reals nil )"bool" convergence_aux "metric_space/" )"bool" pointwise_convergence nil ))nil ))nil 3391989427"" (skosimp)"" (typepred "x!1" )"" (rewrite "pointwise_bounded_def" ) (("" (flatten) nil nil ))nil ))nil ))nil )nil pointwise_convergencenil )"bool" pointwise_convergence nil )nil sequences nil )nil pointwise_convergence nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil pointwise_convergence nil ))nil ))nil 3391989427"" (skosimp)"" (typepred "x!1" )"" (rewrite "pointwise_bounded_def" ) (("" (flatten) nil nil ))nil ))nil ))nil )nil pointwise_convergencenil )"bool" pointwise_convergence nil )nil sequences nil )nil pointwise_convergence nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil pointwise_convergence nil ))nil ))nil 3391989427"" (expand "pointwise_convergent?" )"" (inst + "lambda x: 0" )"" (expand "pointwise_convergence?" )"" (skosimp)"" (rewrite "metric_convergence_def" *)"" (expand "metric_converges_to" )"" (skosimp)"" (inst + "0" ) (("" (grind) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )nil pointwise_convergence nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" metric_space_def"metric_space/" )"bool" sets nil )"set[T]" metric_space_def "metric_space/" )"real" reals nil )"[numfield, numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )"bool" reals nil )nil booleans nil )"real" pointwise_convergence nil )nil sequences nil )nil naturalnumbers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil metric_space"metric_space/" )"bool" pointwise_convergencenil )"bool" pointwise_convergencenil ))nil ))nil 3392121345"" (skosimp*)"" (expand "pointwise_convergence?" )"" (skosimp)"" (inst - "x!1" )"" (inst - "x!1" )"" (rewrite "metric_convergence_def" *)"" (rewrite "metric_convergence_def" *)"" (rewrite "metric_convergence_def" *)"" (expand "metric_converges_to" )"" (skosimp)"" (inst - "r!1/2" )"" (inst - "r!1/2" )"" (skosimp*)"" (inst + "max(n!1,n!2)" )"" "" "i!1" )"" "i!1" )"" assert )"" expand "ball" )"" "" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" pointwise_convergencenil )nil pointwise_convergence nil )nil metric_space"metric_space/" )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )nil sequences nil )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 )AND const-decl "[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield, numfield -> numfield]" number_fields nil )"sequence[[T -> real]]" pointwise_convergence nil )"[T -> real]" real_fun_ops "reals/" )"{s: nonneg_rat | s >= q AND s >= r}" real_defs nil )"{k: nat | i <= k AND j <= k}" nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"metric_open[real, (LAMBDA (x, y: real): abs(x - y))]" "metric_space/" )"(total_order?[real])" nil )"bool" sets nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"set[T]" metric_space_def "metric_space/" )"real" reals nil )"bool" reals nil )nil real_types nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"posreal" nil )"bool" metric_space_def"metric_space/" ))nil 3392121446"" (skosimp)"" (expand "pointwise_convergence?" )"" (skosimp)"" (inst - "x!1" )"" (rewrite "metric_convergence_def" *)"" (rewrite "metric_convergence_def" *)"" (expand "metric_converges_to" )"" (skosimp)"" (expand "ball" )"" (expand "member" )"" (case-replace "c!1=0" )"1" (expand "*" )"1" (expand "*" )"1" (expand "abs" )"1" (propax) nil nil )) nil ))nil ))nil )"2" (inst - "r!1/abs(c!1)" )"1" (skosimp)"1" (inst + "n!1" )"1" "1" "i!1" )"1" assert )"1" expand "*" )"1" expand "*" )"1" rewrite "div_mult_pos_lt2" "1" rewrite "abs_mult" "1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" "posreal_div_posreal_is_posreal" "px" "r!1" "py" "abs(c!1)" ))"2" (assert ) nil nil )) nil ))nil )"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" pointwise_convergencenil )nil pointwise_convergence nil )"sequence[[T -> real]]" pointwise_convergence nil )"[T -> real]" real_fun_ops "reals/" )"bool" sets nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"nzreal" nil )"boolean" notequal nil )"real" pointwise_convergence nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"bool" reals nil )nil real_types nil )"posreal" pointwise_convergence nil )nil real_props nil )"nnreal" nil )nil real_props nil )"(strict_total_order?[real])" real_props nil )nil real_types nil )"real" reals nil )"[T, T -> boolean]" equalities nil )"set[T]" metric_space_def "metric_space/" )"real" reals nil )"bool" metric_space_def"metric_space/" )"[numfield, numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )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 sequences nil )nil naturalnumbers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil metric_space"metric_space/" ))nil 3392115698"" (skosimp)"" "pointwise_convergence_scal" "u" "u!1" "f" "f!1" "c" "-1" ))"" (assert )"" (expand "*" )"" (expand "-" )"" (expand "-" 1)"" (expand "*" -1) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil )nil sequences nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil pointwise_convergence nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil pointwise_convergencenil )"odd_int" integers nil )"[T -> real]" real_fun_ops "reals/" )"sequence[[T -> real]]" pointwise_convergence nil )"real" reals nil )"real" reals nil )"sequence[[T -> real]]" pointwise_convergence nil )"[T -> real]" real_fun_ops "reals/" ))nil 3392115828"" (skosimp)"" (lemma "pointwise_convergence_opp" ("u" "v!1" "f" "f1!1" ))"" (assert )"" "pointwise_convergence_sum" "u" "u!1" "f0" "f0!1" "v" "-v!1" "f1" "-f1!1" ))"" (assert )"" (expand "+" )"" (expand "-" )"" (expand "-" )"" (expand "+" ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil sequences nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil pointwise_convergence nil )nil pointwise_convergencenil )"sequence[[T -> real]]" pointwise_convergence nil )"[T -> real]" real_fun_ops "reals/" )nil pointwise_convergencenil )"[T -> real]" real_fun_ops "reals/" )"sequence[[T -> real]]" pointwise_convergence nil )"real" reals nil )"real" reals nil )"real" reals nil )"sequence[[T -> real]]" pointwise_convergence nil )"[T -> real]" real_fun_ops "reals/" ))nil 3392115342"" (skosimp)"" (typepred "w0!1" )"" (typepred "w1!1" )"" (expand "pointwise_convergent?" )"" (skosimp*)"" (inst + "f!2+f!1" )"" "pointwise_convergence_sum" "u" "w0!1" "v" "w1!1" "f0" "f!2" "f1" "f!1" ))"" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )nil nil )"bool" pointwise_convergence nil )nil sequences nil )nil pointwise_convergence nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"[T -> real]" real_fun_ops "reals/" )nil pointwise_convergencenil ))nil ))nil 3392115342"" (skosimp)"" (typepred "w!1" )"" (expand "pointwise_convergent?" )"" (skosimp)"" (inst + "c!1*f!1" )"" "pointwise_convergence_scal" "u" "w!1" "f" "f!1" "c" "c!1" ))"" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )nil nil )"bool" pointwise_convergence nil )nil sequences nil )nil pointwise_convergence nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil pointwise_convergencenil )"[T -> real]" real_fun_ops "reals/" ))nil ))nil 3392115342"" (skosimp)"" (typepred "w!1" )"" (expand "pointwise_convergent?" )"" (skosimp)"" (inst + "-f!1" )"" "pointwise_convergence_opp" ("u" "w!1" "f" "f!1" ))"" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )nil nil )"bool" pointwise_convergence nil )nil sequences nil )nil pointwise_convergence nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil pointwise_convergencenil )"[T -> real]" real_fun_ops "reals/" ))nil ))nil 3392115342"" (skosimp)"" (typepred "w0!1" )"" (typepred "w1!1" )"" (expand "pointwise_convergent?" )"" (skosimp*)"" (inst + "f!2-f!1" )"" "pointwise_convergence_diff" "u" "w0!1" "v" "w1!1" "f0" "f!2" "f1" "f!1" ))"" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )nil nil )"bool" pointwise_convergence nil )nil sequences nil )nil pointwise_convergence nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"[T -> real]" real_fun_ops "reals/" )nil pointwise_convergencenil ))nil ))nil 3391989427"" (skolem + ("u!1" ))"" (expand "pointwise_bounded?" )"" (expand "pointwise?" )"" (skosimp)"" (rewrite "bounded_seq_def" )"" (typepred "u!1" )"" (expand "pointwise_convergent?" )"" (skosimp)"" (expand "pointwise_convergence?" )"" (inst - "x!1" )"" (rewrite "metric_convergence_def" *)"" (expand "metric_converges_to" )"" (expand "ball" )"" (expand "member" )"" "1" "1" )"1" "1" expand "bounded_above?" )"1" "n!1=0" )"1" "f!1(x!1)+1" )"1" "1" "x!2" )"1" (grind) nil nil ))nil ))nil ))nil )"2" case "forall (i:posnat): nonempty?[real] LAMBDA (n: nat): u!1(n)(x!1), {n | n < i}))AND LAMBDA (n: nat): u!1(n)(x!1), {n | n < i}))") "1" "n!1" )"1" "max(lub(image[nat, real](LAMBDA (n: nat): u!1(n)(x!1), {n | n < n!1})),f!1(x!1)+1)" )"1" "lub(image[nat, real] LAMBDA (n: nat): u!1(n)(x!1),") "1" expand "least_upper_bound?" )"1" "1" expand "upper_bound?" )"1" "1" case "x!2<n!1" )"1" "u!1(x!2)(x!1)" )"1" "1" "LUB" "lub(image[nat, real](LAMBDA (n: nat): u!1(n)(x!1), {n | n < n!1}))" )"1" nil nil ))nil ))nil )"2" expand "image" )"2" "x!2" )nil nil ))nil ))nil )"2" "x!2" )"2" "LUB" "lub(image[nat, real] LAMBDA (n: nat): u!1(n)(x!1), {n | n < n!1}))") "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" replace -1)"2" expand "bounded_above?" )"2" expand "above_bounded" )"2" "2" "n!2" )"2" expand "upper_bound?" )"2" expand "upper_bound" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" assert )"2" expand "above_bounded" )"2" expand "bounded_above?" )"2" "2" "n!2" )"2" expand "upper_bound?" )"2" expand "upper_bound" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil )"2" "2" "i" )"1" (assert ) nil nil )"2" (assert ) nil nil )"3" (assert ) nil nil )"4" "4" "j!1=0" )"1" "1" "1" expand "image" )"1" expand "nonempty?" )"1" expand "empty?" )"1" expand "member" )"1" "u!1(0)(x!1)" )"1" "0" )nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "image" )"2" expand "above_bounded" )"2" expand "upper_bound" )"2" "u!1(0)(x!1)" )"2" "2" "z!1" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" "j!1>0" )"1" "1" "1" expand "nonempty?" )"1" expand "empty?" )"1" expand "image" )"1" expand "member" )"1" "u!1(0)(x!1)" )"1" "0" )nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "above_bounded" )"2" "2" "max(n!2,u!1(j!1)(x!1))" )"2" expand "image" )"2" expand "upper_bound" )"2" "2" "z!1" )"2" "2" "x!2" )"2" "x!2=j!1" )"1" "1" nil nil ))nil )"2" "z!1" )"1" "1" nil nil ))nil )"2" "x!2" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "1" )"2" "2" "n!1>0" )"1" case "forall (i:posnat): nonempty?[real] LAMBDA (n: nat): u!1(n)(x!1), {n | n < i}))AND LAMBDA (n: nat): u!1(n)(x!1), {n | n < i}))") "1" "n!1" )"1" "1" expand "bounded_below?" )"1" "glb(image[nat, real] LAMBDA (n: nat): u!1(n)(x!1),") "1" "GLB" "glb(image[nat, real] LAMBDA (n: nat): u!1(n)(x!1),") "1" "min(GLB,f!1(x!1)-1)" )"1" expand "greatest_lower_bound?" )"1" expand "lower_bound?" )"1" "1" case "x!2<n!1" )"1" "u!1(x!2)(x!1)" )"1" "1" nil nil ))nil )"2" expand "image" )"2" "x!2" )nil nil ))nil ))nil )"2" "x!2" )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" expand "below_bounded" )"2" expand "bounded_below?" )"2" expand "lower_bound?" )"2" expand "lower_bound" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "i" )"1" (assert ) nil nil )"2" (assert ) nil nil )"3" (assert ) nil nil )"4" "4" "j!1=0" )"1" expand "image" )"1" expand "nonempty?" )"1" expand "empty?" )"1" expand "member" )"1" expand "below_bounded" )"1" "1" "1" "u!1(0)(x!1)" )"1" "0" )nil nil ))nil )"2" "u!1(0)(x!1)" )"2" expand "lower_bound" )"2" "2" "z!1" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" case "j!1>0" )"1" "1" "1" expand "nonempty?" )"1" expand "empty?" )"1" "u!1(0)(x!1)" )"1" expand "image" )"1" expand "member" )"1" "0" )nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "image" )"2" expand "below_bounded" )"2" "2" "min(n!2,u!1(j!1)(x!1))" )"2" expand "lower_bound" )"2" "2" "z!1" )"2" "2" "x!2=j!1" )"1" "1" nil nil ))nil )"2" "z!1" )"1" nil nil )"2" "x!2" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "bounded_below?" )"2" "f!1(x!1)-1" )"2" "2" assert )"2" "x!2" )"2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" pointwise_convergence nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" metric_space_def"metric_space/" )"bool" sets nil )"nat" pointwise_convergence nil )"{y: real | EXISTS (x: ({n | n < 1 + j!1})): y = u!1(x)(x!1)}" nil )"({n | n < 1 + j!1})" pointwise_convergencenil )"nat" pointwise_convergence nil )"bool" real_fun_preds "reals/" )"bool" bound_defs "reals/" )"nat" pointwise_convergence nil )"bool" bounded_real_defs nil )"bool" reals nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"{x | greatest_lower_bound?(x, SB)}" nil )"bool" bounded_real_defs nil )"bool" bounded_real_defs nil )"bool" bounded_reals "reals/" )nil real_types nil )"bool" reals nil )"bool" real_fun_preds "reals/" )nil integers nil )nil integers nil )set type-eq-decl nil sets nil )"bool" sets nil )"set[R]" function_image nil )"bool" reals nil )nil defined_types nil )"bool" bounded_reals "reals/" )"pointwise_convergent" pointwise_convergencenil )"T" pointwise_convergence nil )"bool" bounded_real_defs nil )"{x | least_upper_bound?(x, SA)}" bounded_real_defsnil )"bool" bounded_real_defs nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"bool" bound_defs "reals/" )"bool" bounded_real_defs nil )"nat" pointwise_convergence nil )"nat" pointwise_convergence nil )"(strict_total_order?[real])" real_props nil )"[bool, bool -> bool]" booleans nil )nil defined_types nil )nil naturalnumbers nil )"bool" sets nil )"nat" pointwise_convergence nil )"{y: real | EXISTS (x: ({n | n < 1 + j!1})): y = u!1(x)(x!1)}" nil )"({n | n < 1 + j!1})" pointwise_convergencenil )"posint" nil )"posint" nil )"real" reals nil )"[numfield, numfield -> numfield]" number_fields nil )"(total_order?[real])" nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"[T, T -> boolean]" equalities nil )"set[T]" metric_space_def "metric_space/" )"real" reals nil )"[numfield, numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )nil metric_space"metric_space/" )"bool" pointwise_convergencenil )nil nil )"bool" pointwise_convergence nil )nil pointwise_convergence nil )nil sequences nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil convergence_aux "metric_space/" )"bool" pointwise_convergence nil ))nil ))nil 3392116096"" (skosimp)"" (split)"1" (flatten)"1" "pointwise_convergence?(plus(u!1), plus(f!1))" )"1" "pointwise_convergence_diff" "u" "plus(u!1)" "f0" "plus(f!1)" "v" "u!1" "f1" "f!1" ))"1" (assert )"1" (hide -2 -3)"1" (case-replace " plus(f!1) - f!1=minus(f!1)" )"1" (case-replace "plus(u!1) - u!1=minus(u!1)" )"1" (hide-all-but 1)"1" (apply-extensionality :hide? t)"1" (expand "-" )"1" (expand "plus" )"1" (expand "minus" )"1" "1" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (apply-extensionality :hide? t)"2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (expand "pointwise_convergence?" )"2" (skosimp)"2" (inst - "x!1" )"2" (expand "plus" )"2" (expand "plus" )"2" (rewrite "metric_convergence_def" *)"2" (rewrite "metric_convergence_def" *)"2" (expand "metric_converges_to" )"2" (skosimp)"2" expand "ball" )"2" expand "member" )"2" "trichotomy" "x" "f!1(x!1)" ))"2" "1" "max(f!1(x!1), 0)=f!1(x!1)" )"1" "1" "min(r!1,abs(f!1(x!1)))" )"1" "1" "n!1" )"1" "1" "i!1" )"1" assert )"1" expand "max" )"1" "u!1(i!1)(x!1) < 0" )"1" nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" (grind) nil nil ))nil ))nil ))nil )"2" "2" (grind) nil nil ))nil ))nil )"2" replace -1)"2" expand "max" 1 1)"2" assert )"2" "r!1" )"2" "2" "n!1" )"2" "2" "i!1" )"2" assert )"2" rewrite "abs_mult" "2" rewrite "abs_mult" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "max(f!1(x!1), 0)=0" )"1" "1" "min(r!1, abs(f!1(x!1)))" )"1" "1" "n!1" )"1" "1" "i!1" )"1" assert )"1" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" (grind) nil nil ))nil ))nil ))nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" "pointwise_convergence_diff" "u" "plus(u!1)" "f0" "plus(f!1)" "v" "minus(u!1)" "f1" "minus(f!1)" ))"2" (assert )"2" (hide -2 -3)"2" (lemma "plus_minus_def" ("f" "f!1" ))"2" (replace -1 -2 rl)"2" (hide -1)"2" (case-replace "plus(u!1) - minus(u!1)=u!1" )"2" (hide-all-but 1)"2" (apply-extensionality :hide? t)"2" (expand "-" )"2" (expand "plus" )"2" expand "minus" )"2" "plus_minus_def" "f" "u!1(x!1)" ))"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )nil pointwise_convergence nil )nil sequences nil )"bool" pointwise_convergencenil )nil real_types nil )"sequence[[T -> nnreal]]" pointwise_convergencenil )"[T -> nnreal]" real_fun_ops_aux "reals/" )"[T -> nnreal]" real_fun_ops_aux "reals/" )"[T -> real]" real_fun_ops "reals/" )"[T, T -> boolean]" equalities nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"sequence[[T -> real]]" pointwise_convergence nil )"sequence[[T -> nnreal]]" pointwise_convergencenil )nil pointwise_convergencenil )"bool" sets nil )"(total_order?[real])" nil )"bool" reals nil )"T" pointwise_convergence nil )"[T -> real]" pointwise_convergence nil )"posreal" pointwise_convergence nil )nil real_types nil )"bool" reals nil ) (> const-decl "bool" reals nil )"{z: nonneg_real | z <= x AND z <= y}" real_defs nil )"odd_int" integers nil )nil real_props nil )"{j: posint | j >= i}" nil )"nnreal" nil )"real" reals nil )"{k: nat | i <= k AND j <= k}" nil )nil real_axioms nil )"set[T]" metric_space_def "metric_space/" )"bool" metric_space_def"metric_space/" )"[numfield, numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )nil metric_space"metric_space/" )nil real_fun_ops_aux "reals/" ))nil 3392257085"" (skosimp)"" (split)"1" (expand "image" )"1" (expand "nonempty?" )"1" (expand "empty?" )"1" (expand "member" )"1" (inst - "p!1(n!1)(x!1)" )"1" (inst + "n!1" ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (typepred "p!1" )"2" (expand "pointwise_bounded_below?" )"2" (expand "pointwise?" )"2" (inst - "x!1" )"2" (expand "bounded_below?" )"2" (expand "below_bounded" )"2" (expand "lower_bound" )"2" (skosimp)"2" (inst + "a!1" )"2" (skosimp)"2" (typepred "z!1" )"2" (expand "image" )"2" "2" "x!2" )"2" "x!2" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" sets nil )"bool" sets nil )"(total_order?[real])" nil )nil nil )"bool" pointwise_convergencenil )nil sequences nil )nil pointwise_convergence nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"bool" sets nil )"set[R]" function_image nil )"bool" bounded_reals "reals/" )"(total_order?[real])" nil )set type-eq-decl nil sets nil )"bool" bound_defs "reals/" )"bool" real_fun_preds "reals/" )"bool" pointwise_convergence nil )NOT const-decl "[bool -> bool]" booleans nil ))nil ))nil 3392257085"" (skosimp)"" (split)"1" (expand "fullset" )"1" (expand "image" )"1" (expand "nonempty?" )"1" (expand "empty?" )"1" (expand "member" )"1" (inst - "inf(b!1)(0)(x!1)" )"1" (inst + "0" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (typepred "b!1" )"2" (lemma "pointwise_bounded_is_bounded_above" ("x" "b!1" ))"2" (hide -2)"2" (expand "pointwise_bounded_above?" )"2" (expand "pointwise?" )"2" (inst - "x!1" )"2" (expand "bounded_above?" )"2" (expand "fullset" )"2" (expand "image" )"2" (expand "above_bounded" )"2" (skosimp)"2" (expand "upper_bound" )"2" "a!1" )"2" "2" "z!1" )"2" "2" expand "inf" )"2" "inf(image[nat, real](LAMBDA (m:nat): b!1(m)(x!1), {m:nat | m >= x!2}))" )"2" replace -2 * rl)"2" expand "greatest_lower_bound" )"2" "2" expand "lower_bound" )"2" "b!1(x!2)(x!1)" )"1" "x!2" )"1" assert )nil nil ))nil )"2" expand "image" )"2" "x!2" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"set[R]" function_image nil )"bool" sets nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )nil pointwise_convergence nil )nil sequences nil )"bool" pointwise_convergencenil )nil nil )"real" pointwise_convergence nil )"bool" pointwise_convergence nil )nil pointwise_convergencenil )"bool" booleans nil )"bool" sets nil )"bool" sets nil )"set" sets nil )nil nil )"bool" pointwise_convergencenil )"bool" bounded_reals "reals/" )"bool" bound_defs "reals/" )nil defined_types nil )"bool" bound_defs "reals/" )"bool" reals nil ) (set type-eq-decl nil sets nil )nil defined_types nil )"bool" bounded_reals "reals/" )nil bounded_reals "reals/" )"{x | greatest_lower_bound(<=)(x, Sl)}" "reals/" )"bool" bound_defs "reals/" )"(total_order?[real])" nil )"(total_order?[real])" nil )"({x | TRUE})" pointwise_convergence nil )"T" pointwise_convergence nil )"pointwise_bounded" pointwise_convergencenil )"[T, T -> boolean]" equalities nil )"bool" real_fun_preds "reals/" )"bool" pointwise_convergence nil )NOT const-decl "[bool -> bool]" booleans nil ))nil ))nil 3392091014"" (skosimp)"" (split)"1" (expand "image" )"1" (expand "nonempty?" )"1" (expand "empty?" )"1" (expand "member" )"1" (inst - "a!1(n!1)(x!1)" )"1" (inst + "n!1" ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (typepred "a!1" )"2" (expand "pointwise_bounded_above?" )"2" (expand "pointwise?" )"2" (inst - "x!1" )"2" (expand "bounded_above?" )"2" (expand "image" )"2" (expand "above_bounded" )"2" (expand "upper_bound" )"2" (skosimp)"2" (inst + "a!2" )"2" (skosimp)"2" (typepred "z!1" )"2" "2" "x!2" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" sets nil )"bool" sets nil )"(total_order?[real])" nil )nil nil )"bool" pointwise_convergencenil )nil sequences nil )nil pointwise_convergence nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"bool" sets nil )"set[R]" function_image nil )"bool" bound_defs "reals/" )"[T, T -> boolean]" equalities nil )"(total_order?[real])" nil )"bool" bounded_reals "reals/" )"bool" real_fun_preds "reals/" )"bool" pointwise_convergence nil )NOT const-decl "[bool -> bool]" booleans nil ))nil ))nil 3392306597"" (skosimp)"" (split)"1" (expand "fullset" )"1" (expand "image" )"1" (expand "nonempty?" )"1" (expand "empty?" )"1" (expand "member" )"1" (inst - "sup(b!1)(0)(x!1)" )"1" (inst + "0" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (typepred "b!1" )"2" (rewrite "pointwise_bounded_def" )"2" (flatten)"2" (expand "pointwise_bounded_below?" )"2" (expand "pointwise?" )"2" (inst - "x!1" )"2" (hide -1)"2" (expand "bounded_below?" )"2" (expand "fullset" )"2" (expand "image" )"2" (expand "below_bounded" )"2" (expand "lower_bound" )"2" "2" "a!1" )"2" "2" "z!1" )"2" "2" expand "sup" )"2" "sup(image[nat, real](LAMBDA (m:nat): b!1(m)(x!1), {m:nat | m >= x!2}))" )"2" replace -2 * rl)"2" "2" expand "least_upper_bound" )"2" "2" expand "upper_bound" )"2" "b!1(x!2)(x!1)" )"1" "x!2" )"1" assert )nil nil ))nil )"2" expand "image" )"2" "x!2" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"set[R]" function_image nil )"bool" sets nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )nil pointwise_convergence nil )nil sequences nil )"bool" pointwise_convergencenil )nil nil )"real" pointwise_convergence nil )"bool" pointwise_convergence nil )nil pointwise_convergencenil )"bool" booleans nil )"bool" sets nil )"bool" sets nil )"set" sets nil )nil pointwise_convergence nil )"bool" pointwise_convergencenil )"bool" real_fun_preds "reals/" )"bool" bound_defs "reals/" )"[T, T -> boolean]" equalities nil )"bool" bound_defs "reals/" )"(total_order?[real])" nil )"(total_order?[real])" nil )"({x | TRUE})" pointwise_convergence nil )"T" pointwise_convergence nil )"pointwise_bounded" pointwise_convergencenil )"{x | least_upper_bound(<=)(x, Su)}" bounded_reals"reals/" )nil bounded_reals "reals/" )"bool" bounded_reals "reals/" )nil defined_types nil )set type-eq-decl nil sets nil ) (<= const-decl "bool" reals nil )"bool" bound_defs "reals/" )nil defined_types nil )"bool" bounded_reals "reals/" )"bool" pointwise_convergence nil )NOT const-decl "[bool -> bool]" booleans nil ))nil ))nil 3392306597"" (skosimp)"" (typepred "a!1" )"" (expand "pointwise_bounded_above?" )"" (expand "pointwise_bounded_below?" )"" (expand "pointwise?" )"" (skosimp)"" (inst - "x!1" )"" (expand "bounded_below?" )"" (expand "bounded_above?" )"" (skosimp)"" (assert )"" (expand "-" )"" (expand "-" )"" (inst + "-a!2" )"" "" "x!2" )"" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil nil )"bool" pointwise_convergencenil )nil sequences nil )nil pointwise_convergence nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"bool" pointwise_convergencenil )"bool" real_fun_preds "reals/" )"sequence[[T -> real]]" pointwise_convergence nil )"real" reals nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )"(total_order?[real])" nil )"[T -> real]" real_fun_ops "reals/" )"bool" real_fun_preds "reals/" )"bool" pointwise_convergence nil ))nil ))nil 3392306598"" (skosimp)"" (apply-extensionality :hide? t)"" (apply-extensionality :hide? t)"" (expand "inf" )"" (expand "-" )"" (expand "-" )"" (expand "sup" )"" "sup(image[nat, real](LAMBDA m: a!1(m)(x!2), {m | m >= x!1}))" )"" "SUP" "sup(image[nat, real](LAMBDA m: a!1(m)(x!2), {m | m >= x!1}))" )"" "inf(image[nat, real] LAMBDA (m_1: nat): -a!1(m_1)(x!2),") "" "INF" "inf(image[nat, real] LAMBDA (m_1: nat): -a!1(m_1)(x!2),") "" (expand "image" )"" (expand "greatest_lower_bound" )"" (expand "least_upper_bound" )"" expand "upper_bound" )"" expand "lower_bound" )"" "" "-INF" )"" "1" "-SUP" )"1" "1" (assert ) nil nil )"2" (assert ) nil nil )"3" "3" "z!1" )"3" "3" "-z!1" )"1" assert )nil nil )"2" "x!3" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil )"3" "3" "z!1" )"3" "3" "-z!1" )"1" "both_sides_times_neg_le1" "nz" "-1" ))"1" "-z!1" "INF" )"1" assert )nil nil ))nil ))nil )"2" "x!3" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )nil pointwise_convergence nil )"real" pointwise_convergence nil )nil nil )"bool" pointwise_convergencenil )"sequence[[T -> real]]" pointwise_convergence nil )"real" pointwise_convergence nil )nil nil )"bool" pointwise_convergencenil )nil sequences nil )"[T -> real]" real_fun_ops "reals/" )"set[R]" function_image nil )"{x | least_upper_bound(<=)(x, Su)}" bounded_reals"reals/" )nil bounded_reals "reals/" )"bool" bounded_reals "reals/" )nil defined_types nil )"bool" sets nil )set type-eq-decl nil sets nil ) (<= const-decl "bool" reals nil )"bool" bound_defs "reals/" )nil defined_types nil )NOT const-decl "[bool -> bool]" booleans nil )"real" reals nil )"bool" bound_defs "reals/" )"bool" bounded_reals "reals/" )nil bounded_reals "reals/" )"{x | greatest_lower_bound(<=)(x, Sl)}" "reals/" )nil number_fields nil )"[numfield -> numfield]" number_fields nil )"bool" bound_defs "reals/" )"odd_int" integers nil )nil real_props nil )nil real_types nil )"bool" reals nil )nil real_types nil )"{y: real | EXISTS (x: ({m | m >= x!1})): y = a!1(x)(x!2)}" nil )"{y: real | EXISTS (x: ({m_1: nat | m_1 >= x!1})): y = -a!1(x)(x!2)}" nil )"T" pointwise_convergence nil )"pointwise_bounded_above" nil )"nat" pointwise_convergence nil )"(total_order?[real])" nil )"bool" bound_defs "reals/" )"[T, T -> boolean]" equalities nil ))nil 3392306597"" (skosimp)"" (typepred "b!1" )"" (rewrite "pointwise_bounded_def" )"" (rewrite "pointwise_bounded_def" )"" (flatten)"" (expand "pointwise_bounded_above?" )"" (expand "pointwise_bounded_below?" )"" (expand "pointwise?" )"" (split)"1" (skosimp)"1" (hide -1)"1" (inst - "x!1" )"1" (expand "bounded_below?" )"1" (expand "bounded_above?" )"1" "1" assert )"1" "-a!1" )"1" "1" "x!2" )"1" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp)"2" (inst - "x!1" )"2" (hide -2)"2" (expand "bounded_above?" )"2" (expand "bounded_below?" )"2" "2" assert )"2" "-a!1" )"2" "2" "x!2" )"2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil pointwise_convergencenil )"bool" pointwise_convergence nil )nil sequences nil )nil pointwise_convergence nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"sequence[[T -> real]]" pointwise_convergence nil )"bool" pointwise_convergencenil )"bool" pointwise_convergence nil )"bool" real_fun_preds "reals/" )"real" reals nil )"[T -> real]" real_fun_ops "reals/" )"(total_order?[real])" nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )"real" reals nil )"bool" real_fun_preds "reals/" )"bool" pointwise_convergencenil )nil pointwise_convergence nil ))nil ))nil 3392307047"" (skosimp)"" (apply-extensionality :hide? t)"" (expand "liminf" )"" (expand "limsup" )"" (expand "-" )"" (expand "-" )"" "inf(image[nat, real](LAMBDA m: sup(b!1)(m)(x!1), fullset[nat]))" )"" "INF" "inf(image[nat, real] LAMBDA m: sup(b!1)(m)(x!1),") "" "sup(image[nat, real] LAMBDA (m_1: nat):LAMBDA n: LAMBDA (x: T): -b!1(n)(x))(m_1)(x!1),") "1" "SUP" "sup(image[nat, real] LAMBDA (m_1: nat):LAMBDA n: LAMBDA (x: T): -b!1(n)(x))(m_1)(x!1),") "1" (expand "fullset" )"1" (expand "image" )"1" (expand "least_upper_bound" )"1" (expand "greatest_lower_bound" )"1" expand "lower_bound" )"1" expand "upper_bound" )"1" "1" "-INF" )"1" "-SUP" )"1" "1" "1" (assert ) nil nil )"2" (assert ) nil nil )"3" assert )"3" "3" "z!1" )"3" "3" "-z!1" )"1" assert )nil nil )"2" assert )"2" rewrite "sup_inf_def" "2" expand "-" )"2" expand "-" )"2" "x!2" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil )"3" "3" "z!1" )"3" "3" "-z!1" )"1" assert )nil nil )"2" "x!2" )"2" replace -1)"2" rewrite "sup_inf_def" "2" expand "-" )"2" expand "-" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (typepred "b!1" )"2" (rewrite "pointwise_bounded_def" )"2" (flatten)"2" (hide-all-but (-1 1))"2" (expand "pointwise_bounded_above?" )"2" expand "pointwise_bounded_below?" )"2" expand "pointwise?" )"2" "2" "x!2" )"2" expand "bounded_below?" )"2" expand "bounded_above?" )"2" "2" "-a!1" )"2" "2" "x!3" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil pointwise_convergence nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"sequence[[T -> real]]" pointwise_convergence nil )"real" pointwise_convergence nil )"[T -> real]" real_fun_ops "reals/" )"real" pointwise_convergence nil )nil pointwise_convergencenil )"bool" pointwise_convergence nil )nil sequences nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"[T, T -> boolean]" equalities nil )"bool" pointwise_convergence nil )"bool" real_fun_preds "reals/" )"real" reals nil )"bool" real_fun_preds "reals/" )nil pointwise_convergence nil )"bool" bound_defs "reals/" )"bool" booleans nil )"pointwise_bounded" pointwise_convergencenil )"T" pointwise_convergence nil )"{y: real | LAMBDA n: LAMBDA (x: T): -b!1(n)(x))(x_1)(x!1)}" nil )nil pointwise_convergence nil )"(total_order?[real])" nil )"{y: real | EXISTS (x_1: ({x | TRUE})): y = sup(b!1)(x_1)(x!1)}" nil )"bool" bound_defs "reals/" )"[numfield -> numfield]" number_fields nil )nil number_fields nil )"real" pointwise_convergence nil )nil nil )"bool" pointwise_convergencenil )"{x | least_upper_bound(<=)(x, Su)}" bounded_reals"reals/" )nil bounded_reals "reals/" )"bool" bounded_reals "reals/" )"bool" bound_defs "reals/" )"real" reals nil )NOT const-decl "[bool -> bool]" booleans nil )nil defined_types nil )"bool" bound_defs "reals/" )"bool" reals nil ) (set type-eq-decl nil sets nil )"bool" sets nil )nil defined_types nil )"bool" bounded_reals "reals/" )nil bounded_reals "reals/" )"{x | greatest_lower_bound(<=)(x, Sl)}" "reals/" )"set[R]" function_image nil )"bool" pointwise_convergencenil )nil nil )"real" pointwise_convergence nil )"set" sets nil ))nil 3392295604"" (skosimp)"" (expand "pointwise_increasing?" )"" (skosimp)"" (expand "increasing?" )"" (skosimp)"" (expand "inf" 1 2)"" "inf(image[nat, real](LAMBDA m: p!1(m)(x!1), {m | m >= y!1}))" )"" "INF" "inf(image[nat, real] LAMBDA m: p!1(m)(x!1),") "" (expand "greatest_lower_bound" )"" (flatten)"" (expand "image" )"" (expand "lower_bound" )"" (inst -2 "inf(p!1)(x!2)(x!1)" )"" (split -2)"1" (propax) nil nil )"2" (assert ) nil nil )"3" "3" "z!1" )"3" "3" "x!3" )"3" "3" expand "inf" )"3" "inf(image[nat, real](LAMBDA m: p!1(m)(x!1), {m | m >= x!2}))" )"3" "LHS" "inf(image[nat, real](LAMBDA m: p!1(m)(x!1), {m | m >= x!2}))" )"3" expand "image" )"3" expand "greatest_lower_bound" )"3" "3" expand "lower_bound" )"3" "z!1" )"3" "x!3" )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" pointwise_convergence nil )"bool" real_fun_preds "reals/" )"real" pointwise_convergence nil )"[T, T -> boolean]" equalities nil )"bool" bound_defs "reals/" )"(total_order?[real])" nil )"(total_order?[real])" nil )"({m | m >= y!1})" pointwise_convergencenil )"{y: real | EXISTS (x: ({m | m >= y!1})): y = p!1(x)(x!1)}" nil )"T" pointwise_convergence nil )"pointwise_bounded_below" nil )"nat" pointwise_convergence nil )"nat" pointwise_convergence nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil defined_types nil )"bool" bound_defs "reals/" )"bool" reals nil ) (set type-eq-decl nil sets nil )"bool" sets nil )nil defined_types nil )"bool" bounded_reals "reals/" )nil bounded_reals "reals/" )"{x | greatest_lower_bound(<=)(x, Sl)}" "reals/" )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"set[R]" function_image nil )nil pointwise_convergence nil )nil sequences nil )"bool" pointwise_convergencenil )nil nil ))nil 3392296131"" (skosimp)"" (expand "inf" )"" "inf(image[nat, real](LAMBDA m: p!1(m)(x!1), {m | m >= n!1}))" )"" "INF" "inf(image[nat, real](LAMBDA m: p!1(m)(x!1), {m | m >= n!1}))" )"" (expand "image" )"" (expand "greatest_lower_bound" )"" (flatten)"" (expand "lower_bound" )"" (inst - "p!1(n!1)(x!1)" )"" (inst + "n!1" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" pointwise_convergence nil )"[T, T -> boolean]" equalities nil )"bool" bound_defs "reals/" )"(total_order?[real])" nil )"T" pointwise_convergence nil )"pointwise_bounded_below" nil )"nat" pointwise_convergence nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil defined_types nil )"bool" bound_defs "reals/" )"bool" reals nil ) (set type-eq-decl nil sets nil )"bool" sets nil )nil defined_types nil )"bool" bounded_reals "reals/" )nil bounded_reals "reals/" )"{x | greatest_lower_bound(<=)(x, Sl)}" "reals/" )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"set[R]" function_image nil )nil pointwise_convergence nil )nil sequences nil )"bool" pointwise_convergencenil )nil nil ))nil 3392296352"" (skosimp*)"" (expand "pointwise_convergence?" )"" (inst - "x!1" )"" (lemma "inf_pointwise_increasing" ("p" "p!1" ))"" (expand "pointwise_increasing?" )"" (inst - "x!1" )"" (rewrite "metric_convergence_def" *)"" (case "inf(p!1)(n!1)(x!1)>f!1(x!1)" )"1" (hide 1)"1" (expand "metric_converges_to" )"1" (expand "ball" )"1" (expand "member" )"1" (inst - "inf(p!1)(n!1)(x!1)-f!1(x!1)" )"1" (skosimp)"1" "max(n!1,n!2)" )"1" assert )"1" assert )"1" expand "increasing?" )"1" "n!1" "max(n!1,n!2)" )"1" assert )"1" "INF1" "inf(p!1)(n!1)(x!1)" )"1" "inf_le" "p" "p!1" "n" "max(n!1, n!2)" "x" "x!1" ))"1" "INF2" "inf(p!1)(max(n!1, n!2))(x!1)" )"1" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" pointwise_convergencenil )nil nil )"bool" pointwise_convergencenil )nil sequences nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil pointwise_convergencenil )"bool" reals nil )"real" pointwise_convergence nil )"bool" metric_space_def"metric_space/" )"bool" sets nil )"bool" real_fun_preds "reals/" )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil pointwise_convergence nil )"real" reals nil )"odd_int" integers nil )"[T, T -> boolean]" equalities nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"{k: nat | i <= k AND j <= k}" nil )"{s: nonneg_rat | s >= q AND s >= r}" real_defs nil )nil real_types nil )"[T -> real]" pointwise_convergence nil )"T" pointwise_convergence nil )"nat" pointwise_convergence nil )"pointwise_bounded_below" nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"set[T]" metric_space_def "metric_space/" )"real" reals nil )"[numfield, numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )nil metric_space"metric_space/" )"bool" pointwise_convergence nil )nil pointwise_convergence nil ))nil 3392258310"" (skosimp)"" (expand "pointwise_convergence?" )"" (skosimp)"" (lemma "inf_pointwise_increasing" ("p" "b!1" ))"" (expand "pointwise_increasing?" )"" (inst - "x!1" )"" (rewrite "metric_convergence_def" *)"" (expand "metric_converges_to" )"" (skosimp)"" (expand "ball" )"" (expand "member" )"" (expand "limsup" )"" "sup(image[nat, real] LAMBDA m: inf(b!1)(m)(x!1), fullset[nat]))") "1" "LIMSUP" "sup(image[nat, real] LAMBDA m: inf(b!1)(m)(x!1), fullset[nat]))") "1" expand "least_upper_bound" )"1" "1" expand "upper_bound" )"1" case "EXISTS (n_1: nat): ") "1" "1" "n!1" )"1" "1" "i!1" )"1" "inf(b!1)(i!1)(x!1)" )"1" expand "abs" )"1" assert )nil nil ))nil )"2" expand "fullset" )"2" expand "image" )"2" "i!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "LIMSUP-r!1" )"2" assert )"2" "2" "z!1" )"2" expand "fullset" )"2" expand "image" )"2" "n!1" ))"2" case "inf(b!1)(n!1)(x!1)>LIMSUP - r!1" )"1" "1" "n!1" )"1" "1" expand "increasing?" )"1" "n!1" "i!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" "1" expand "fullset" )"1" expand "image" )"1" expand "nonempty?" )"1" expand "empty?" )"1" expand "member" )"1" "inf(b!1)(0)(x!1)" )"1" "0" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "b!1" )"2" "pointwise_bounded_is_bounded_above" "x" "b!1" ))"2" "2" expand "pointwise_bounded_above?" )"2" expand "pointwise?" )"2" "x!1" )"2" expand "bounded_above?" )"2" expand "above_bounded" )"2" expand "fullset" )"2" expand "image" )"2" expand "upper_bound" )"2" "2" "a!1" )"2" "2" "z!1" )"2" "2" "x!2" )"2" assert )"2" expand "inf" )"2" "inf(image[nat, real](LAMBDA (m:nat): b!1(m)(x!1), {m:nat | m >= x!2}))" )"2" replace "2" expand "greatest_lower_bound" )"2" "2" expand "lower_bound" )"2" "2" "b!1(x!2)(x!1)" )"1" assert )nil nil )"2" expand "image" )"2" "x!2" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" pointwise_convergencenil )nil pointwise_convergencenil )"bool" pointwise_convergence nil )nil nil )"bool" pointwise_convergencenil )nil sequences nil )nil pointwise_convergence nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil pointwise_convergencenil )"bool" metric_space_def"metric_space/" )"real" reals nil )"set[T]" metric_space_def "metric_space/" )"bool" pointwise_convergence nil )"bool" real_fun_preds "reals/" )"({x | TRUE})" pointwise_convergence nil )"bool" bound_defs "reals/" )"{x | greatest_lower_bound(<=)(x, Sl)}" "reals/" )nil bounded_reals "reals/" )"bool" bounded_reals "reals/" )"bool" bound_defs "reals/" )"bool" pointwise_convergencenil )nil nil )"bool" sets nil )"[T, T -> boolean]" equalities nil )"odd_int" integers nil )"[bool, bool -> bool]" booleans nil )"bool" reals nil ) (> const-decl "bool" reals nil )nil real_types nil )"bool" booleans nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"nat" pointwise_convergence nil )"T" pointwise_convergence nil )"pointwise_bounded" pointwise_convergencenil )"(strict_total_order?[real])" real_props nil )"bool" real_fun_preds "reals/" )"bool" bound_defs "reals/" )"set" sets nil )"set[R]" function_image nil )"{x | least_upper_bound(<=)(x, Su)}" bounded_reals"reals/" )nil bounded_reals "reals/" )"bool" bounded_reals "reals/" )nil defined_types nil )"bool" sets nil )set type-eq-decl nil sets nil ) (<= const-decl "bool" reals nil )"bool" bound_defs "reals/" )nil defined_types nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" sets nil )"[numfield, numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )"real" pointwise_convergence nil )"real" pointwise_convergence nil )nil metric_space"metric_space/" )"bool" pointwise_convergencenil ))nil 3392259265"" (skosimp)"" "pointwise_convergent_is_pointwise_bounded" ("x" "p!1" ))"1" (expand "pointwise_converges_upto?" )"1" (lemma "inf_pointwise_increasing" ("p" "p!1" ))"1" (lemma "limsup_pointwise_convergence" ("b" "p!1" ))"1" "extensionality" ("f" "f!1" "g" "limsup(p!1)" ))"1" (split -1)"1" (assert ) nil nil )"2" (hide 2)"2" (skosimp)"2" "inf_pointwise_le" ("p" "p!1" "f" "f!1" ))"2" (assert )"2" (expand "limsup" )"2" "sup(image[nat, real](LAMBDA m: inf(p!1)(m)(x!1), fullset[nat]))" )"2" (expand "pointwise_convergence?" )"2" "x!1" )"2" "x!1" )"2" "LIMSUP" "sup(image[nat, real](LAMBDA m: inf(p!1)(m)(x!1), fullset[nat]))" )"2" expand "least_upper_bound" )"2" "2" expand "fullset" )"2" expand "image" )"2" expand "upper_bound" )"2" "trich_lt" "x" "f!1(x!1)" "y" "LIMSUP" ))"2" "1" "f!1(x!1)" )"1" assert )"1" "1" "1" "z!1" )"1" "1" "x!2" "x!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil )"3" "3" rewrite "metric_convergence_def" "3" rewrite "metric_convergence_def" "3" expand "metric_converges_to" "3" "(f!1(x!1)-LIMSUP)/2" )"1" "1" expand "ball" )"1" expand "member" )"1" case "forall (i:nat): i >= n!1=> p!1(i)(x!1)>LIMSUP+(f!1(x!1) - LIMSUP) / 2" )"1" "1" expand "pointwise_increasing?" )"1" "x!1" )"1" expand "increasing?" )"1" "n!1" "_" )"1" "INF" "inf(p!1)(n!1)(x!1)" )"1" replace "1" expand "inf" "1" "inf(image[nat, real](LAMBDA m: p!1(m)(x!1), {m | m >= n!1}))" )"1" replace "1" expand "greatest_lower_bound" )"1" expand "image" "1" "1" expand "lower_bound" )"1" "LIMSUP + (f!1(x!1) - LIMSUP) / 2" )"1" "INF" )"1" "1" assert )nil nil )"2" assert )nil nil )"3" "3" "z!1" )"3" "3" "x!2" )"3" "x!2" )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "INF" )"2" "n!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "i!1" )"2" assert )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil )"2" (expand "pointwise_convergent?" )"2" (inst + "f!1" ) nil nil )) nil ))nil ))nil )nil nil )"bool" pointwise_convergencenil )nil nil )"bool" pointwise_convergence nil )nil sequences nil )nil pointwise_convergence nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil nil )nil pointwise_convergencenil )nil functions nil )"real" pointwise_convergence nil )nil pointwise_convergence nil )"bool" pointwise_convergencenil )"bool" bound_defs "reals/" )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"bool" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )nil metric_space"metric_space/" )"bool" metric_space_def"metric_space/" )"bool" sets nil )"bool" bound_defs "reals/" )"bool" bounded_reals "reals/" )nil bounded_reals "reals/" )"{x | greatest_lower_bound(<=)(x, Sl)}" "reals/" )"real" pointwise_convergence nil )"bool" bound_defs "reals/" )"bool" real_fun_preds "reals/" )"bool" pointwise_convergence nil )"[numfield, numfield -> numfield]" number_fields nil )"[bool, bool -> bool]" booleans nil )"real" reals nil )"set[T]" metric_space_def "metric_space/" )nil real_types nil )"bool" reals nil )"{x | LAMBDA m: inf(p!1)(m)(x!1), fullset[nat]))}" nil )"pointwise_bounded_below" nil )"T" pointwise_convergence nil )"[T -> real]" pointwise_convergence nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )"real" reals nil )"(total_order?[real])" nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )nil real_props nil )"[T, T -> boolean]" equalities nil )NOT const-decl "[bool -> bool]" booleans nil )nil defined_types nil )"bool" bound_defs "reals/" )"bool" reals nil ) (set type-eq-decl nil sets nil )"bool" sets nil )nil defined_types nil )"bool" bounded_reals "reals/" )nil bounded_reals "reals/" )"{x | least_upper_bound(<=)(x, Su)}" bounded_reals"reals/" )"set[R]" function_image nil )"real" pointwise_convergence nil )"set" sets nil )nil pointwise_convergencenil )"bool" pointwise_convergence nil )nil nil )"bool" pointwise_convergencenil ))nil 3392257085"" (skosimp)"" (expand "pointwise_bounded_below?" )"" (expand "pointwise?" )"" (skosimp)"" (expand "bounded_below?" )"" (inst + "0" )"" (skosimp)"" (expand "plus" )"" (expand "plus" )"" (hide -1) (("" (grind) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" pointwise_convergencenil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"sequence[[T -> nnreal]]" pointwise_convergencenil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"[T -> nnreal]" real_fun_ops_aux "reals/" )"bool" real_fun_preds "reals/" )"bool" pointwise_convergence nil ))nil ))nil 3392257085"" (skosimp)"" (hide -1 -2)"" (expand "pointwise_bounded_below?" )"" (expand "pointwise?" )"" (expand "bounded_below?" )"" (skosimp)"" (inst + "0" )"" (skosimp) (("" (grind) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" pointwise_convergence nil )"[T -> nnreal]" real_fun_ops_aux "reals/" )nil pointwise_convergence nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"sequence[[T -> nnreal]]" pointwise_convergencenil )"(total_order?[real])" nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"bool" real_fun_preds "reals/" )"bool" pointwise_convergencenil ))nil ))nil 3392296765"" (skosimp)"" (rewrite "plus_minus_pointwise_convergence" )"" (flatten)"" "inf_pointwise_convergence_upto" "p" "plus(u!1)" "f" "plus(f!1)" ))"1" "inf_pointwise_convergence_upto" "p" "minus(u!1)" "f" "minus(f!1)" ))"1" (assert ) nil nil )"2" (hide-all-but 1)"2" (expand "pointwise_bounded_below?" )"2" (expand "pointwise?" )"2" (skosimp)"2" (expand "bounded_below?" )"2" (expand "bounded_below?" )"2" (inst + "0" ) (("2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (expand "pointwise_bounded_below?" )"2" (expand "pointwise?" )"2" (skosimp)"2" (expand "bounded_below?" )"2" (expand "bounded_below?" )"2" (inst + "0" ) (("2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil nil )nil pointwise_convergence nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )nil sequences nil )"sequence[[T -> nnreal]]" pointwise_convergencenil )nil nil )"bool" pointwise_convergencenil )"[T -> nnreal]" real_fun_ops_aux "reals/" )nil real_types nil )nil nil )"bool" pointwise_convergence nil )"bool" real_fun_preds "reals/" )"real" reals nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )NOT const-decl "[bool -> bool]" booleans nil )"sequence[[T -> nnreal]]" pointwise_convergencenil )"[T -> nnreal]" real_fun_ops_aux "reals/" )"(strict_total_order?[real])" real_props nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil ))
Messung V0.5 in Prozent C=100 H=99 G=99
¤ Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.0.158Bemerkung:
(vorverarbeitet am 2026-04-30)
¤ *Bot Zugriff
2026-05-26
