| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/measure_integration/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 254 kB |
|
Impressum integral_convergence_scaf.prfInteraktion undPortierbarkeitLisp |
|||||||||||||||
|
(integral_convergence_scaf (monotone_convergence_scaf 0 (monotone_convergence_scaf-1 nil 3409476910 ("" (case "FORALL (F: sequence[nn_integrable], f: [T -> nnreal]): pointwise_converges_upto?(F, f)&bounded?(nn_integral o F) =>(nn_integrable?(f) AND converges_upto?((nn_ (("1" (skosimp) (("1" (inst - "lambda (n:nat): F!1(n)-F!1(0)" "f!1-F!1(0)") (("1" (split -1) (("1" (flatten) (("1" (lemma "nn_integrable_is_integrable") (("1" (inst - "f!1 - F!1(0)") (("1" (lemma "integrable_add" ("f1" "f!1 - F!1(0)" "f2" "F!1(0)")) (("1" (case-replace "((+[T])(f!1 - F!1(0), F!1(0)))=f!1") (("1" (hide -1) (("1" (replace -1) (("1" (expand "o ") (("1" (expand "converges_upto?") (("1" (flatten) (("1" (split) (("1" (rewrite "integral_nn" -4 :dir rl) (("1" (rewrite "integral_diff") (("1" (rewrite "metric_convergence_def") (("1" (rewrite "metric_convergence_def") (("1" (expand "metric_converges_to") (("1" (skosimp) (("1" (inst - "r!1") (("1" (skosimp) (("1" (inst + "n!1") (("1" (skosimp) (("1" (inst - "i!1") (("1" (assert) (("1" (rewrite "integral_nn" -5 :dir rl) (("1" (rewrite "integral_diff") (("1" (assert) (("1" (expand "ball") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skolem + ("n!1")) (("2" (lemma "integrable_diff" ("f1" "F!1(n!1)" "f2" "F!1(0)")) (("2" (lemma "nn_integrable_is_nn_integrable" ("f" "(-[T])(F!1(n!1), F!1(0))")) (("2" (case-replace "(FORALL (x1: T): ((-[T])(F!1(n!1), F!1(0)))(x1) >= 0)") (("2" (expand "pointwise_converges_upto?") (("2" (flatten) (("2" (hide-all-but (1 -9)) (("2" (skosimp) (("2" (expand "-") (("2" (expand "pointwise_increasing?") (("2" (inst - "x1!1") (("2" (expand "increasing?") (("2" (inst - "0" "n!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "increasing?") (("2" (skolem + ("i!1" "j!1")) (("2" (flatten) (("2" (inst - "i!1" "j!1") (("2" (assert) (("2" (hide -5 -8 -3 -4) (("2" (rewrite "integral_nn" -3 :dir rl) (("2" (rewrite "integral_nn" -3 :dir rl) (("2" (rewrite "integral_diff") (("2" (rewrite "integral_diff") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (apply-extensionality :hide? t) (("2" (expand "+") (("2" (expand "-") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "pointwise_converges_upto?") (("2" (flatten) (("2" (split) (("1" (expand "pointwise_convergence?") (("1" (skosimp) (("1" (inst - "x!1") (("1" (rewrite "metric_convergence_def") (("1" (rewrite "metric_convergence_def") (("1" (expand "metric_converges_to") (("1" (skosimp) (("1" (inst - "r!1") (("1" (skosimp) (("1" (inst + "n!1") (("1" (skosimp) (("1" (inst - "i!1") (("1" (expand "ball") (("1" (assert) (("1" (expand "-") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "pointwise_increasing?") (("2" (skosimp) (("2" (inst - "x!1") (("2" (expand "increasing?") (("2" (skolem + ("i!1" "j!1")) (("2" (flatten) (("2" (inst - "i!1" "j!1") (("2" (expand "-") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (expand "o ") (("3" (expand "bounded?") (("3" (flatten) (("3" (split) (("1" (expand "bounded_above?") (("1" (skosimp) (("1" (expand "pointwise_converges_upto?") (("1" (flatten) (("1" (hide -1) (("1" (expand "bounded_below?") (("1" (skosimp) (("1" (inst + "a!1-a!2") (("1" (skolem + ("n!1")) (("1" (inst - "n!1") (("1" (inst - "0") (("1" (rewrite "integral_nn" 1 :dir rl) (("1" (rewrite "integral_diff") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "bounded_below?") (("2" (skosimp) (("2" (expand "bounded_above?") (("2" (expand "pointwise_converges_upto?") (("2" (flatten) (("2" (hide -1) (("2" (skosimp) (("2" (inst + "a!1-a!2") (("2" (skolem + ("n!1")) (("2" (inst - "0") (("2" (inst - "n!1") (("2" (rewrite "integral_nn" 1 :dir rl) (("2" (rewrite "integral_diff") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp) (("2" (expand "-") (("2" (expand "pointwise_converges_upto?") (("2" (expand "pointwise_increasing?") (("2" (flatten) (("2" (inst - "x1!1") (("2" (hide -3) (("2" (expand "pointwise_convergence?") (("2" (inst - "x1!1") (("2" (rewrite "metric_convergence_def") (("2" (expand "metric_converges_to") (("2" (inst - "F!1(0)(x1!1)-f!1(x1!1)") (("1" (skosimp) (("1" (expand "ball") (("1" (expand "member") (("1" (inst - "n!1") (("1" (assert) (("1" (expand "increasing?") (("1" (inst - "0" "n!1") (("1" (assert) 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) ("3" (hide 2) (("3" (skosimp) (("3" (split) (("1" (skosimp) (("1" (expand "pointwise_converges_upto?") (("1" (flatten) (("1" (expand "pointwise_increasing?") (("1" (inst - "x1!1") (("1" (expand "increasing?") (("1" (inst - "0" "n!1") (("1" (expand "-") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "integrable_diff" ("f1" "F!1(n!1)" "f2" "F!1(0)")) (("2" (expand "pointwise_converges_upto?") (("2" (flatten) (("2" (rewrite "nn_integrable_is_nn_integrable") (("2" (skosimp) (("2" (expand "pointwise_increasing?") (("2" (inst - "x!1") (("2" (expand "-") (("2" (expand "increasing?") (("2" (inst - "0" "n!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp) (("2" (lemma "pointwise_measurable" ("u" "F!1" "f" "f!1")) (("2" (split -1) (("1" (name "ISF" "lambda (n:nat): choose({u:increasing_nn_isf | pointwise_convergence?(u,F!1(n))})") (("1" (hide -1) (("1" (case "forall (n:nat): increasing_nn_isf?(ISF(n))") (("1" (case "forall (n:nat): pointwise_convergence?(ISF(n), F!1(n))") (("1" (name "G" "lambda (n:nat): maximum(lambda (i:nat): ISF(i)(n),n)") (("1" (case "forall (n:nat,x:T): G(n)(x)<=F!1(n)(x)") (("1" (case "forall (n:nat, x: T): F!1(n)(x)<=f!1(x)") (("1" (case "forall (n:nat,x:T): 0 <= G(n)(x)") (("1" (case "pointwise_increasing?(G)") (("1" (case "nonempty?({nn:nn_isf | exists (n:nat): nn = G(n)})") (("1" (case "pointwise_bounded_above?(G)") (("1" (case "pointwise_converges_upto?(G, f!1)") (("1" (case-replace "nn_integrable?(f!1)") (("1" (expand "converges_upto?") (("1" (case-replace "increasing?(nn_integral o F!1)") (("1" (case "convergence?((nn_integral o G), nn_integral(f!1))") (("1" (expand "pointwise_converges_upto?") (("1" (flatten) (("1" (rewrite "metric_convergence_def") (("1" (rewrite "metric_convergence_def") (("1" (case "forall (n:nat): (nn_integral o G)(n)<=(nn_integral o F!1)(n)") (("1" (case "increasing?(nn_integral o G)") (("1" (case "forall (n:nat): (nn_integral o F!1)(n)<=nn_integral(f!1)") (("1" (name-replace "LIMIT" "nn_integral(f!1)") (("1" (name-replace "INT_F" "nn_integral o F!1") (("1" (name-replace "INT_G" "nn_integral o G") (("1" (hide-all-but (-1 -2 -3 -4 -5 1)) (("1" (expand "metric_converges_to") (("1" (skosimp) (("1" (inst -4 "r!1") (("1" (skosimp) (("1" (inst + "n!1") (("1" (skosimp) (("1" (inst -4 "i!1") (("1" (expand "ball") (("1" (assert) (("1" (inst - "i!1") (("1" (expand "abs") (("1" (inst - "i!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 -5 -12)) (("2" (skosimp) (("2" (expand "o ") (("2" (lemma "nn_integrable_le" ("g" "F!1(n!1)" "f" "f!1")) (("2" (split -1) (("1" (flatten) nil nil) ("2" (skosimp) (("2" (inst - "n!1" "x!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 -6 -10)) (("2" (expand "pointwise_increasing?") (("2" (expand "increasing?") (("2" (expand "o ") (("2" (skolem + ("i!1" "j!1")) (("2" (flatten) (("2" (lemma "nn_integrable_le" ("g" "G(i!1)" "f" "G(j!1)")) (("2" (split -1) (("1" (flatten) nil nil) ("2" (hide 2) (("2" (skosimp) (("2" (inst - "x!1") (("2" (inst - "i!1" "j!1") (("2" (inst - "i!1" "x!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 -9 -11)) (("2" (skosimp) (("2" (expand "o ") (("2" (lemma "nn_integrable_le" ("g" "G(n!1)" "f" "F!1(n!1)")) (("2" (split -1) (("1" (flatten) nil nil) ("2" (skosimp) (("2" (inst - "n!1" "x!1") (("2" (inst - "n!1" "x!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "pointwise_converges_upto?") (("2" (flatten) (("2" (hide -1 -14 -15 -16 -17 -11) (("2" (copy -1) (("2" (expand "nn_integrable?" -1) (("2" (skosimp) (("2" (lemma "nn_convergence" ("u1" "u!1" "f" "f!1" "u2" "choose({u:increasing_nn_isf | pointwise_convergence?(u,f!1)})")) (("1" (replace -2) (("1" (replace -3) (("1" (split -1) (("1" (flatten) (("1" (expand "nn_integral" 1 2) (("1" (replace -2 1 rl) (("1" (hide -2) (("1" (hide -1) (("1" (lemma "nn_convergence" ("u1" "u!1" "f" "f!1" "u2" "G")) (("1" (replace -2) (("1" (replace -3) (("1" (replace -5) (("1" (flatten) (("1" (replace -2) (("1" (expand "o" 1 1) (("1" (case-replace "(LAMBDA (x: nat): nn_integral(G(x)))=isf_integral o G") (("1" (rewrite "hausdorff_convergence.limit_def" 1 :dir rl) nil nil) ("2" (hide 2) (("2" (apply-extensionality :hide? t) (("1" (expand "o" 1) (("1" (rewrite "nn_integral_isf") (("1" (expand "nn_isf?") (("1" (skosimp) (("1" (inst -11 "x!1" "x!2") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "o") (("2" (skolem + "n!1") (("2" (lemma "isf_integral_pos" ("i" "G(n!1)")) (("2" (assert) (("2" (skosimp) (("2" (inst - "n!1" "x!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skolem + "n!1") (("3" (split) (("1" (skosimp) (("1" (inst - "n!1" "x1!1") (("1" (assert) nil nil)) nil)) nil) ("2" (lemma "nn_isf_is_nn_integrable" ("x" "G(n!1)")) (("1" (assert) nil nil) ("2" (expand "nn_isf?") (("2" (skosimp) (("2" (inst - "n!1" "x!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (split) (("1" (skolem + "n!1") (("1" (expand "nn_isf?") (("1" (skosimp) (("1" (inst - "n!1" "x!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "increasing_nn_isf?") (("2" (propax) nil nil)) nil)) nil)) nil) ("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (typepred "choose({u: increasing_nn_isf | pointwise_convergence?(u, f!1)})") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 -2 1)) (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (inst - "u!1") (("2" (expand "member") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skolem + ("n!1")) (("3" (assert) (("3" (split) (("1" (skosimp) (("1" (inst - "n!1" "x2!1") (("1" (assert) nil nil)) nil)) nil) ("2" (typepred "G(n!1)") (("2" (lemma "nn_isf_is_nn_integrable" ("x" "G(n!1)")) (("1" (assert) nil nil) ("2" (expand "nn_isf?") (("2" (skosimp) (("2" (inst -8 "n!1" "x!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "pointwise_converges_upto?") (("2" (flatten) (("2" (hide-all-but (-15 1)) (("2" (expand "pointwise_increasing?") (("2" (expand "increasing?") (("2" (expand "o ") (("2" (skolem + ("i!1" "j!1")) (("2" (flatten) (("2" (lemma "nn_integrable_le" ("g" "F!1(i!1)" "f" "F!1(j!1)")) (("2" (split -1) (("1" (flatten) nil nil) ("2" (hide 2) (("2" (skosimp) (("2" (inst - "x!1") (("2" (inst - "i!1" "j!1") (("2" (assert) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "nn_integrable?") (("2" (inst + "G") (("1" (expand "pointwise_converges_upto?") (("1" (flatten) (("1" (assert) (("1" (lemma "bounded_above_is_convergent" ("u" "isf_integral o G")) (("1" (split -1) (("1" (expand "convergent_upto?") (("1" (skosimp) (("1" (expand "converges_upto?") (("1" (flatten) (("1" (expand "convergent?") (("1" (inst + "x!1") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-15 1 -8 -2 -6)) (("2" (expand "bounded?") (("2" (flatten) (("2" (expand "bounded_above?") (("2" (skosimp) (("2" (expand "o" -4) (("2" (inst + "a!1") (("2" (skosimp) (("2" (expand "o" +) (("2" (typepred "G(x!1)") (("2" (lemma "nn_integral_isf" ("i" "G(x!1)")) (("1" (replace -1 1 rl) (("1" (hide -1) (("1" (lemma "nn_integrable_le" ("g" "G(x!1)" "f" "F!1(x!1)")) (("1" (split -1) (("1" (flatten) (("1" (inst -7 "x!1") (("1" (assert) nil nil)) nil)) nil) ("2" (skosimp) (("2" (inst -3 "x!1" "x!2") (("2" (assert) (("2" (inst -4 "x!1" "x!2") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "nn_isf?") (("2" (skosimp) (("2" (inst -3 "x!1" "x!2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but (-2 1)) (("3" (expand "pointwise_increasing?") (("3" (expand "increasing?") (("3" (expand "o ") (("3" (skolem + ("i!1" "j!1")) (("3" (flatten) (("3" (lemma "isf_integral_le" ("i1" "G(i!1)" "i2" "G(j!1)")) (("3" (split -1) (("1" (propax) nil nil) ("2" (skosimp) (("2" (inst - "x!1") (("2" (inst - "i!1" "j!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (split) (("1" (skosimp) (("1" (assert) (("1" (expand "nn_isf?") (("1" (skosimp) (("1" (inst -5 "x1!1" "x!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "increasing_nn_isf?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "pointwise_converges_upto?") (("2" (assert) (("2" (expand "pointwise_convergence?") (("2" (skosimp) (("2" (typepred "sup(Im(LAMBDA (n:nat): G(n)(x!1)))") (("1" (name-replace "SUP" "sup(Im(LAMBDA (n:nat): G(n)(x!1)))") (("1" (expand "Im") (("1" (case-replace "SUP=f!1(x!1)") (("1" (expand "least_upper_bound") (("1" (flatten) (("1" (hide-all-but (-2 -3 -6 1)) (("1" (name-replace "LIMIT" "f!1(x!1)") (("1" (rewrite "metric_convergence_def") (("1" (expand "metric_converges_to") (("1" (skosimp) (("1" (expand "ball") (("1" (expand "member") (("1" (inst - "LIMIT-r!1") (("1" (assert) (("1" (expand "upper_bound" 1) (("1" (skosimp) (("1" (typepred "z!1") (("1" (skolem - ("n!1")) (("1" (replace -1) (("1" (inst + "n!1") (("1" (skosimp) (("1" (expand "pointwise_increasing?") (("1" (inst - "x!1") (("1" (expand "increasing?") (("1" (inst - "n!1" "i!1") (("1" (assert) (("1" (expand "upper_bound") (("1" (inst - "G(i!1)(x!1)") (("1" (assert) (("1" (expand "abs") (("1" (assert) nil nil)) nil)) nil) ("2" (inst + "i!1") 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) ("2" (hide 2) (("2" (lemma "converges_upto_is_lub" ("x" "SUP" "u" "lambda (n:nat): G(n)(x!1)")) (("2" (case-replace "least_upper_bound?(SUP, image[nat, real] (LAMBDA (n:nat): G(n)(x!1), fullset[nat]))") (("1" (hide -1) (("1" (expand "converges_upto?") (("1" (expand "pointwise_increasing?") (("1" (inst -5 "x!1") (("1" (replace -5) (("1" (expand "pointwise_bounded_above?") (("1" (expand "pointwise?") (("1" (inst -3 "x!1") (("1" (assert) (("1" (inst -13 "x!1") (("1" (inst -14 "x!1") (("1" (inst - "_" "x!1") (("1" (inst - "_" "x!1") (("1" (inst - "_" "x!1") (("1" (hide -9) (("1" (case-replace "convergence?(LAMBDA (n:nat): G(n)(x!1), f!1(x!1))") (("1" (lemma "hausdorff_convergence.unique_limit" ("u" "LAMBDA (n:nat): G(n)(x!1)" "l1" "SUP" "l2" "f!1(x!1)")) (("1" (assert) nil nil)) nil) ("2" (hide 2 -1 -2 -3 -4) (("2" (rewrite "metric_convergence_def") (("2" (rewrite "metric_convergence_def") (("2" (case "forall (n:nat): metric_converges_to(LAMBDA (n_1: nat): ISF(n)(n_1)(x!1), F!1(n)(x!1)) (("1" (hide -6) (("1" (expand "metric_converges_to") (("1" (expand "ball") (("1" (expand "member") (("1" (skosimp) (("1" (inst -8 "r!1/2") (("1" (skosimp) (("1" (inst - "n!1") (("1" (inst - "r!1/2") (("1" (skosimp) (("1" (inst + "n!1+n!2") (("1" (skosimp) (("1" (inst - "i!1") (("1" (assert) (("1" (inst-cp -9 "n!1") (("1" (assert) (("1" (inst-cp -5 "n!1") (("1" (expand "abs" (1 -11)) (("1" (assert) (("1" (inst-cp -7 "i!1") (("1" (assert) (("1" (inst-cp -5 "i!1") (("1" (assert) (("1" (case "forall (i:nat): ISF(n!1)(i)(x!1)<=F!1(n!1)(x!1)") (("1" (inst - "i!1") (("1" (expand "abs" -2) (("1" (assert) (("1" (case "ISF(n!1)(i!1)(x!1)<=G(i!1)(x!1)") (("1" (assert) nil nil) ("2" (hide 2) (("2" (expand "G" 1) (("2" (hide-all-but (-3 1)) (("2" (case "forall (j:nat): ISF(n!1)(i!1)(x!1) <= maximum(LAMBDA (i: nat): ISF(i)(i!1), n!1+j)(x!1)" (("1" (inst - "i!1-n!1") (("1" (assert) nil nil)) nil) ("2" (hide 2) (("2" (induct "j") (("1" (case-replace "n!1=0") (("1" (expand "maximum") (("1" (assert) nil nil)) nil) ("2" (expand "maximum") (("2" (assert) (("2" (expand "max") (("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "maximum" 1) (("2" (expand "max") (("2" (name-replace "DRL1" "maximum(LAMBDA (i: nat): ISF(i)(i!1), n!1 + j!1)(x!1)") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp) (("2" (expand "ISF" 1) (("2" (hide-all-but 1) (("2" (typepred "choose({u: increasing_nn_isf | pointwise_convergence?(u, F!1(n!1))})") (("1" (name-replace "DRL" "choose({u: increasing_nn_isf | pointwise_convergence?(u, F!1(n!1))})") (("1" (expand "increasing_nn_isf?") (("1" (expand "pointwise_increasing?") (("1" (expand "pointwise_convergence?") (("1" (inst - "x!1") (("1" (inst - "x!1") (("1" (rewrite "metric_convergence_def") (("1" (expand "metric_converges_to") (("1" (inst - "DRL(i!2)(x!1) - F!1(n!1)(x!1)") (("1" (skosimp) (("1" (expand "ball") (("1" (expand "member") (("1" (inst - "i!2+n!3") (("1" (assert) (("1" (expand "increasing?") (("1" (inst - "i!2" "i!2+n!3") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (expand "member") (("2" (typepred "F!1(n!1)") (("2" (expand "nn_integrable?") (("2" (skosimp) (("2" (inst - "u!1") 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) ("2" (hide-all-but (-5 1)) (("2" (skosimp) (("2" (inst - "n!1") (("2" (inst - "x!1") (("2" (rewrite "metric_convergence_def") 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" (hide-all-but (-2 1)) (("2" (expand "fullset") (("2" (expand "image") (("2" (expand "least_upper_bound?") (("2" (expand "least_upper_bound") (("2" (flatten) (("2" (split) (("1" (hide -2) (("1" (expand "upper_bound") (("1" (expand "upper_bound?") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (hide -1) (("2" (skosimp) (("2" (inst - "y!1") (("2" (split -2) (("1" (propax) nil nil) ("2" (assert) nil nil) ("3" (hide 2) (("3" (expand "upper_bound?") (("3" (expand "upper_bound") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 1)) (("2" (expand "Im") (("2" (expand "pointwise_bounded_above?") (("2" (expand "pointwise?") (("2" (inst - "x!1") (("2" (expand "bounded_above?") (("2" (expand "above_bounded") (("2" (skosimp) (("2" (expand "upper_bound") (("2" (inst + "ceiling(a!1)") (("2" (skosimp) (("2" (typepred "z!1") (("2" (skosimp) (("2" (inst - "x!2") (("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) ("2" (hide 2) (("2" (expand "pointwise_bounded_above?") (("2" (expand "pointwise?") (("2" (skosimp) (("2" (expand "bounded_above?") (("2" (inst + "f!1(x!1)") (("2" (skosimp) (("2" (inst -5 "x!2" "x!1") (("2" (inst -4 "x!2" "x!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (inst - "G(0)") (("1" (expand "member") (("1" (inst + "0") nil nil)) nil) ("2" (expand "nn_isf?") (("2" (skosimp) (("2" (inst - "0" "x!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2 -9 -7 -4) (("2" (expand "pointwise_increasing?") (("2" (skosimp) (("2" (expand "increasing?") (("2" (expand "G") (("2" (case "forall (i,j,k,n:nat): j<=k => maximum(LAMBDA (i: nat): ISF(i)(j), i)(x!1) <= maximum(LAMBDA ( (("1" (skosimp) (("1" (inst - "x!2" "x!2" "y!1" "y!1-x!2") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil) ("2" (hide 2 -1 -2 -3 -4 -6) (("2" (induct "n") (("1" (induct "i") (("1" (skosimp) (("1" (expand "maximum") (("1" (inst - "0") (("1" (expand "increasing_nn_isf?") (("1" (expand "pointwise_increasing?") (("1" (inst - "x!1") (("1" (expand "increasing?") (("1" (inst - "j!1" "k!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skolem!) (("2" (flatten) (("2" (skosimp) (("2" (expand "maximum" 1) (("2" (expand "max") (("2" (inst - "j!2" "k!1") (("2" (assert) (("2" (name-replace "DRL1" "maximum(LAMBDA (i: nat): ISF(i)(j!2), j!1)(x!1)") (("2" (name-replace "DRL2" "maximum(LAMBDA (i: nat): ISF(i)(k!1), j!1)(x!1)") (("2" (inst - "1+j!1") (("2" (expand "increasing_nn_isf?") (("2" (expand "pointwise_increasing?") (("2" (inst - "x!1") (("2" (expand "increasing?") (("2" (inst - "j!2" "k!1") (("2" (assert) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skolem!) (("2" (flatten) (("2" (induct "i") (("1" (skosimp) (("1" (expand "maximum" 1) (("1" (expand "max") (("1" (inst - "0" "j!2" "k!1") (("1" (assert) (("1" (name-replace "DRL1" "maximum(LAMBDA (i: nat): ISF(i)(k!1), j!1)(x!1)") (("1" (expand "maximum") (("1" (hide -3) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "maximum" 1) (("2" (expand "max") (("2" (inst - "j!3" "k!1") (("2" (assert) (("2" (case "forall (n:nat): ISF(1 + j!2)(j!3)(x!1)<=maximum(LAMBDA (i: nat): ISF(i)(k!1), 1 + n + j!2)(x (("1" (inst - "j!1") (("1" (name-replace "DRL1" "maximum(LAMBDA (i: nat): ISF(i)(k!1), 1 + j!1 + j!2)(x!1)") (("1" (name-replace "DRL2" "maximum(LAMBDA (i: nat): ISF(i)(j!3), j!2)(x!1)") (("1" (hide -4 -5 -3) (("1" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (hide -1 2 -3) (("2" (induct "n") (("1" (expand "maximum") (("1" (expand "max") (("1" (inst - "1+j!2") (("1" (expand "increasing_nn_isf?") (("1" (expand "pointwise_increasing?") (("1" (inst - "x!1") (("1" (expand "increasing?") (("1" (inst - "j!3" "k!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "maximum" 1) (("2" (expand "max") (("2" (name-replace "DRL1" "maximum(LAMBDA (i: nat): ISF(i)(k!1), 1 + j!4 + j!2)(x!1)") (("2" (hide -3) (("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)) nil)) nil) ("2" (hide 2) (("2" (hide-all-but 1) (("2" (expand "G") (("2" (case "FORALL (n,j:nat,x:T): 0 <= maximum(LAMBDA (i: nat): ISF(i)(j), n)(x)") (("1" (skosimp) (("1" (inst - "n!1" "n!1" "x!1") nil nil)) nil) ("2" (hide 2) (("2" (skolem + ("_" "j!1" "x!1")) (("2" (induct "n") (("1" (expand "maximum") (("1" (typepred "ISF(0)(j!1)") (("1" (expand "nn_isf?") (("1" (inst - "x!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "maximum" 1) (("2" (expand "max") (("2" (typepred "ISF(1+j!2)(j!1)") (("2" (expand "nn_isf?") (("2" (inst - "x!1") (("2" (expand "max") (("2" (case-replace "ISF(1 + j!2)(j!1)(x!1) < maximum(LAMBDA (i: nat): ISF(i)(j!1), j!2)(x!1)") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-6 1)) (("2" (skosimp) (("2" (expand "pointwise_converges_upto?") (("2" (expand "pointwise_convergence?") (("2" (expand "pointwise_increasing?") (("2" (flatten) (("2" (inst - "x!1") (("2" (inst - "x!1") (("2" (expand "increasing?") (("2" (rewrite "metric_convergence_def") (("2" (expand "metric_converges_to") (("2" (inst - "F!1(n!1)(x!1)-f!1(x!1)") (("1" (skosimp) (("1" (inst - "n!1+n!2") (("1" (expand "ball") (("1" (expand "member") (("1" (inst - "n!1" "n!1+n!2") (("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) ("2" (expand "pointwise_converges_upto?") (("2" (flatten) (("2" (hide -1 -4 -5 -7 2) (("2" (expand "G") (("2" (case "forall (k,n:nat,x:T): maximum(LAMBDA (i: nat): ISF(i)(k), n)(x) <= F!1(n)(x)") (("1" (skosimp) (("1" (inst - "n!1" "n!1" "x!1") nil nil)) nil) ("2" (hide 2) (("2" (induct "n") (("1" (skosimp) (("1" (expand "maximum") (("1" (inst - "0") (("1" (inst - "0") (("1" (hide -3) (("1" (expand "increasing_nn_isf?") (("1" (expand "pointwise_convergence?") (("1" (expand "pointwise_increasing?") (("1" (inst - "x!1") (("1" (inst - "x!1") (("1" (rewrite "metric_convergence_def") (("1" (expand "metric_converges_to") (("1" (inst - "ISF(0)(k!1)(x!1) - F!1(0)(x!1)") (("1" (skosimp) (("1" (expand "ball") (("1" (expand "member") (("1" (expand "abs") (("1" (inst - "n!1+k!1") (("1" (assert) (("1" (expand "increasing?") (("1" (inst - "k!1" "n!1+k!1") (("1" (assert) (("1" (assert) 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)) nil) ("2" (skosimp*) (("2" (expand "maximum" 1) (("2" (expand "max") (("2" (inst - "k!1" "x!1") (("2" (name-replace "MAXI" "maximum(LAMBDA (i: nat): ISF(i)(k!1), j!1)(x!1)") (("2" (expand "pointwise_increasing?") (("2" (inst -4 "x!1") (("2" (expand "increasing?") (("2" (inst -4 "j!1" "1+j!1") (("2" (assert) (("2" (case "ISF(1 + j!1)(k!1)(x!1)<=F!1(1 + j!1)(x!1)") (("1" (expand "max") (("1" (case-replace "ISF(1 + j!1)(k!1)(x!1) < MAXI") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil) ("2" (hide -1 2 -4) (("2" (inst - "1+j!1") (("2" (inst - "1+j!1") (("2" (expand "increasing_nn_isf?") (("2" (expand "pointwise_convergence?") (("2" (expand "pointwise_increasing?") (("2" (inst - "x!1") (("2" (inst - "x!1") (("2" (rewrite "metric_convergence_def") (("2" (expand "metric_converges_to") (("2" (inst - "ISF(1 + j!1)(k!1)(x!1) - F!1(1 + j!1)(x!1)") (("1" (skosimp) (("1" (expand "ball") (("1" (expand "member") (("1" (inst - "n!1+k!1") (("1" (expand "increasing?") (("1" (inst - "k!1" "k!1+n!1") (("1" (assert) (("1" (assert) 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)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2 -2 -4) (("2" (skosimp) (("2" (typepred "ISF(n!1)") (("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (typepred "ISF(n!1)") (("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp) (("2" (expand "nonempty?") (("2" (hide -2 -3 -4) (("2" (typepred "F!1(n!1)") (("2" (expand "nn_integrable?") (("2" (skosimp) (("2" (expand "empty?") (("2" (inst - "u!1") (("2" (expand "member") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "pointwise_converges_upto?") (("2" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((pointwise_measurable formula-decl nil measure_space nil) (measurable_function? const-decl "bool" measure_space_def nil) (measurable_function nonempty-type-eq-decl nil measure_space_def nil) (choose const-decl "(p)" sets nil) (nonempty? const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (increasing_nn_isf nonempty-type-eq-decl nil nn_integral nil) (increasing_nn_isf? const-decl "bool" nn_integral nil) (nn_isf nonempty-type-eq-decl nil nn_integral nil) (nn_isf? const-decl "bool" nn_integral nil) (isf nonempty-type-eq-decl nil isf nil) (isf? const-decl "bool" isf nil) (isf_maximum application-judgement "isf[T, S, m]" integral_convergence_scaf nil) (maximum def-decl "[T -> real]" real_fun_ops_aux "reals/") (minus_real_is_real application-judgement "real" reals nil) (x!1 skolem-const-decl "T" integral_convergence_scaf nil) (k!1 skolem-const-decl "nat" integral_convergence_scaf nil) (j!1 skolem-const-decl "nat" integral_convergence_scaf nil) (k!1 skolem-const-decl "nat" integral_convergence_scaf nil) (x!1 skolem-const-decl "T" integral_convergence_scaf nil) (pointwise_bounded_above? const-decl "bool" pointwise_convergence nil) (integer nonempty-type-from-decl nil integers nil) (< const-decl "bool" reals nil) (ceiling const-decl "{i | x <= i & i < x + 1}" floor_ceil nil) (upper_bound const-decl "bool" bound_defs "reals/") (x!1 skolem-const-decl "T" integral_convergence_scaf nil) (i!1 skolem-const-decl "nat" integral_convergence_scaf nil) (converges_upto_is_lub formula-decl nil convergence_aux "metric_space/") (upper_bound? const-decl "bool" bounded_real_defs nil) (pointwise? const-decl "bool" pointwise_convergence nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (ISF skolem-const-decl "[n: nat -> ({u: increasing_nn_isf | pointwise_convergence?(u, F!1(n))})]" integral_convergence_scaf nil) (i!2 skolem-const-decl "nat" integral_convergence_scaf nil) (DRL skolem-const-decl "({u: increasing_nn_isf | pointwise_convergence?(u, F!1(n!1))})" integral_convergence_scaf nil) (n!1 skolem-const-decl "nat" integral_convergence_scaf nil) (F!1 skolem-const-decl "sequence[nn_integrable]" integral_convergence_scaf nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (isf_max application-judgement "isf[T, S, m]" integral_convergence_scaf nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (max const-decl "[T -> real]" real_fun_ops_aux "reals/") (nat_induction formula-decl nil naturalnumbers nil) (int_minus_int_is_int application-judgement "int" integers nil) (int_plus_int_is_int application-judgement "int" integers nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (unique_limit formula-decl nil hausdorff_convergence "topology/") (least_upper_bound? const-decl "bool" bounded_real_defs nil) (image const-decl "set[R]" function_image nil) (fullset const-decl "set" sets nil) (Im const-decl "setof[real]" real_fun_props "reals/") (sup const-decl "{x | least_upper_bound(<=)(x, Su)}" bounded_reals "reals/") (sup_set type-eq-decl nil bounded_reals "reals/") (above_bounded const-decl "bool" bounded_reals "reals/") (least_upper_bound const-decl "bool" bound_defs "reals/") (pred type-eq-decl nil defined_types nil) (nonempty_image application-judgement "(nonempty?[real])" double_nn_sequence "extended_nnreal/") (empty? const-decl "bool" sets nil) (nn_isf_is_nn_integrable judgement-tcc nil nn_integral nil) (isf_integral_pos formula-decl nil isf nil) (nn_integral_isf formula-decl nil nn_integral nil) (G skolem-const-decl "[nat -> isf[T, S, m]]" integral_convergence_scaf nil) (limit const-decl "T" topological_convergence "topology/") (convergent type-eq-decl nil topological_convergence "topology/") (convergent? const-decl "bool" topological_convergence "topology/") (limit_def formula-decl nil hausdorff_convergence "topology/") (isf_integral const-decl "real" isf nil) (NOT const-decl "[bool -> bool]" booleans nil) (nn_convergence formula-decl nil nn_integral nil) (nn_integrable_le formula-decl nil nn_integral nil) (convergence? const-decl "bool" topological_convergence "topology/") (metric_induced_topology const-decl "setofsets[T]" metric_space_def "metric_space/") (metric_space_is_hausdorff? name-judgement "(hausdorff?)" convergence_aux "metric_space/") (metric_space_is_hausdorff name-judgement "hausdorff[real]" convergence_aux "metric_space/") (metric_induced_topology_is_second_countable name-judgement "second_countable" real_topology "metric_space/") (convergent_upto? const-decl "bool" convergence_aux "metric_space/") (isf_integral_le formula-decl nil isf nil) (bounded_above_is_convergent formula-decl nil convergence_aux "metric_space/") (y!1 skolem-const-decl "nat" integral_convergence_scaf nil) (x!2 skolem-const-decl "nat" integral_convergence_scaf nil) (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (n!1 skolem-const-decl "nat" integral_convergence_scaf nil) (x!1 skolem-const-decl "T" integral_convergence_scaf nil) (f!1 skolem-const-decl "[T -> nnreal]" integral_convergence_scaf nil) (<= const-decl "bool" reals nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (x1!1 skolem-const-decl "T" integral_convergence_scaf nil) (nn_integrable_is_integrable judgement-tcc nil integral nil) (integrable_add judgement-tcc nil integral nil) (integral_nn formula-decl nil integral nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (integral const-decl "real" integral nil) (metric_convergence_def formula-decl nil metric_space "metric_space/") (integrable_diff judgement-tcc nil integral nil) (pointwise_increasing? const-decl "bool" pointwise_convergence nil) (increasing? const-decl "bool" real_fun_preds "reals/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (nn_integrable_is_nn_integrable formula-decl nil integral nil) (metric_converges_to const-decl "bool" metric_space_def "metric_space/") (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (ball const-decl "set[T]" metric_space_def "metric_space/") (member const-decl "bool" sets nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (ball_is_metric_open application-judgement "metric_open[real, (LAMBDA (x, y: real): abs(x - y))]" convergence_aux "metric_space/") (real_minus_real_is_real application-judgement "real" reals nil) (integral_diff formula-decl nil integral nil) (= const-decl "[T, T -> boolean]" equalities nil) (+ const-decl "[T -> real]" real_fun_ops "reals/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (pointwise_convergence? const-decl "bool" pointwise_convergence nil) (bounded_above? const-decl "bool" real_fun_preds "reals/") (bounded_below? const-decl "bool" real_fun_preds "reals/") (f!1 skolem-const-decl "[T -> real]" integral_convergence_scaf nil) (F!1 skolem-const-decl "sequence[integrable]" integral_convergence_scaf nil) (integrable nonempty-type-eq-decl nil integral nil) (integrable? const-decl "bool" integral nil) (- const-decl "[T -> real]" real_fun_ops "reals/") (integrable_diff application-judgement "integrable" integral_convergence_scaf nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (T formal-type-decl nil integral_convergence_scaf nil) (nnreal type-eq-decl nil real_types nil) (setof type-eq-decl nil defined_types nil) (setofsets type-eq-decl nil sets nil) (sigma_algebra? const-decl "bool" subset_algebra_def nil) (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil) (S formal-const-decl "sigma_algebra" integral_convergence_scaf nil) (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (measure? const-decl "bool" generalized_measure_def nil) (measure_type nonempty-type-eq-decl nil generalized_measure_def nil) (m formal-const-decl "measure_type" integral_convergence_scaf nil) (nn_integrable? const-decl "bool" nn_integral nil) (nn_integrable nonempty-type-eq-decl nil nn_integral nil) (sequence type-eq-decl nil sequences nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (pointwise_converges_upto? const-decl "bool" pointwise_convergence nil) (bounded? const-decl "bool" real_fun_preds "reals/") (O const-decl "T3" function_props nil) (nn_integral const-decl "nnreal" nn_integral nil) (converges_upto? const-decl "bool" convergence_aux "metric_space/")) shostak)))
¤ 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.221Bemerkung: (vorverarbeitet am 2026-04-27) ¤*Bot Zugriff |
|
||||||||||||||
2026-05-26