Impressum integral_convergence_scaf.prf
Sprache: Lisp
(integral_convergence_scafnil 3409476910"" case "FORALL (F: sequence[nn_integrable], f: [T -> nnreal]): AND converges_upto?((nn_integral o F), nn_integral(f)))") "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" "integrable_add" "f1" "f!1 - F!1(0)" "f2" "F!1(0)" ))"1" "((+[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" "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" "1" "r!1" )"1" "1" "n!1" )"1" "1" "i!1" )"1" assert )"1" rewrite "integral_nn" "1" rewrite "integral_diff" )"1" assert )"1" expand "ball" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "n!1" ))"2" "integrable_diff" "f1" "F!1(n!1)" "f2" "F!1(0)" ))"2" "nn_integrable_is_nn_integrable" "f" "(-[T])(F!1(n!1), F!1(0))" ))"2" "(FORALL (x1: T): ((-[T])(F!1(n!1), F!1(0)))(x1) >= 0)" )"2" expand "pointwise_converges_upto?" )"2" "2" "2" "2" expand "-" )"2" expand "pointwise_increasing?" )"2" "x1!1" )"2" expand "increasing?" )"2" "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" "i!1" "j!1" ))"2" "2" "i!1" "j!1" )"2" assert )"2" "2" rewrite "integral_nn" "2" rewrite "integral_nn" "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" "1" "r!1" )"1" "1" "n!1" )"1" "1" "i!1" )"1" expand "ball" )"1" assert )"1" expand "-" )"1" 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" "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" "1" "a!1-a!2" )"1" "n!1" ))"1" "n!1" )"1" "0" )"1" rewrite "integral_nn" "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" "2" "2" "a!1-a!2" )"2" "n!1" ))"2" "0" )"2" "n!1" )"2" rewrite "integral_nn" "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" "F!1(0)(x1!1)-f!1(x1!1)" )"1" "1" expand "ball" )"1" expand "member" )"1" "n!1" )"1" assert )"1" expand "increasing?" )"1" "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" "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" "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" "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" "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" "nn_integrable?(f!1)" )"1" expand "converges_upto?" )"1" "increasing?(nn_integral o F!1)" )"1" case "convergence?((nn_integral o G), nn_integral(f!1))" )"1" expand "pointwise_converges_upto?" )"1" "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" "LIMIT" "nn_integral(f!1)" )"1" "INT_F" "nn_integral o F!1" )"1" "INT_G" "nn_integral o G" )"1" "1" expand "metric_converges_to" )"1" "1" "r!1" )"1" "1" "n!1" )"1" "1" "i!1" )"1" expand "ball" )"1" assert )"1" "i!1" )"1" expand "abs" )"1" "i!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "o " )"2" "nn_integrable_le" "g" "F!1(n!1)" "f" "f!1" ))"2" "1" nil nil )"2" "2" "n!1" "x!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "pointwise_increasing?" )"2" expand "increasing?" )"2" expand "o " )"2" "i!1" "j!1" ))"2" "2" "nn_integrable_le" "g" "G(i!1)" "f" "G(j!1)" ))"2" "1" nil nil )"2" "2" "2" "x!1" )"2" "i!1" "j!1" )"2" "i!1" "x!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "o " )"2" "nn_integrable_le" "g" "G(n!1)" "f" "F!1(n!1)" ))"2" "1" nil nil )"2" "2" "n!1" "x!1" )"2" "n!1" "x!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "pointwise_converges_upto?" )"2" "2" "2" "2" expand "nn_integrable?" "2" "2" "nn_convergence" "u1" "u!1" "f" "f!1" "u2" "choose({u:increasing_nn_isf | pointwise_convergence?(u,f!1)})" ))"1" replace "1" replace "1" "1" "1" expand "nn_integral" "1" replace "1" "1" "1" "nn_convergence" "u1" "u!1" "f" "f!1" "u2" "G" ))"1" replace "1" replace "1" replace "1" "1" replace "1" expand "o" "1" "(LAMBDA (x: nat): nn_integral(G(x)))=isf_integral o G" )"1" rewrite "hausdorff_convergence.limit_def" nil nil )"2" "2" "1" expand "o" "1" rewrite "nn_integral_isf" )"1" expand "nn_isf?" )"1" "1" "x!1" "x!2" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "o" )"2" "n!1" )"2" "isf_integral_pos" "i" "G(n!1)" ))"2" assert )"2" "2" "n!1" "x!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "n!1" )"3" "1" "1" "n!1" "x1!1" )"1" assert )nil nil ))nil ))nil )"2" "nn_isf_is_nn_integrable" "x" "G(n!1)" ))"1" assert )nil nil )"2" expand "nn_isf?" )"2" "2" "n!1" "x!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "1" "n!1" )"1" expand "nn_isf?" )"1" "1" "n!1" "x!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" expand "increasing_nn_isf?" )"2" nil nil ))nil ))nil ))nil )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "choose({u: increasing_nn_isf ") "2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "nonempty?" )"2" expand "empty?" )"2" "u!1" )"2" expand "member" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "n!1" ))"3" assert )"3" "1" "1" "n!1" "x2!1" )"1" assert )nil nil ))nil ))nil )"2" "G(n!1)" )"2" "nn_isf_is_nn_integrable" "x" "G(n!1)" ))"1" assert )nil nil )"2" expand "nn_isf?" )"2" "2" "n!1" "x!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "pointwise_converges_upto?" )"2" "2" "2" expand "pointwise_increasing?" )"2" expand "increasing?" )"2" expand "o " )"2" "i!1" "j!1" ))"2" "2" "nn_integrable_le" "g" "F!1(i!1)" "f" "F!1(j!1)" ))"2" "1" nil nil )"2" "2" "2" "x!1" )"2" "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" "2" expand "nn_integrable?" )"2" "G" )"1" expand "pointwise_converges_upto?" )"1" "1" assert )"1" "bounded_above_is_convergent" "u" "isf_integral o G" ))"1" "1" expand "convergent_upto?" )"1" "1" expand "converges_upto?" )"1" "1" expand "convergent?" )"1" "x!1" )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "bounded?" )"2" "2" expand "bounded_above?" )"2" "2" expand "o" "2" "a!1" )"2" "2" expand "o" "2" "G(x!1)" )"2" "nn_integral_isf" "i" "G(x!1)" ))"1" replace "1" "1" "nn_integrable_le" "g" "G(x!1)" "f" "F!1(x!1)" ))"1" "1" "1" "x!1" )"1" assert )nil nil ))nil ))nil )"2" "2" "x!1" "x!2" )"2" assert )"2" "x!1" "x!2" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "nn_isf?" )"2" "2" "x!1" "x!2" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" expand "pointwise_increasing?" )"3" expand "increasing?" )"3" expand "o " )"3" "i!1" "j!1" ))"3" "3" "isf_integral_le" "i1" "G(i!1)" "i2" "G(j!1)" ))"3" "1" nil nil )"2" "2" "x!1" )"2" "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" "1" "1" assert )"1" expand "nn_isf?" )"1" "1" "x1!1" "x!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "increasing_nn_isf?" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "pointwise_converges_upto?" )"2" assert )"2" expand "pointwise_convergence?" )"2" "2" "sup(Im(LAMBDA (n:nat): G(n)(x!1)))" )"1" "SUP" "sup(Im(LAMBDA (n:nat): G(n)(x!1)))" )"1" expand "Im" )"1" "SUP=f!1(x!1)" )"1" expand "least_upper_bound" )"1" "1" "1" "LIMIT" "f!1(x!1)" )"1" rewrite "metric_convergence_def" )"1" expand "metric_converges_to" )"1" "1" expand "ball" )"1" expand "member" )"1" "LIMIT-r!1" )"1" assert )"1" expand "upper_bound" "1" "1" "z!1" )"1" "n!1" ))"1" replace "1" "n!1" )"1" "1" expand "pointwise_increasing?" )"1" "x!1" )"1" expand "increasing?" )"1" "n!1" "i!1" )"1" assert )"1" expand "upper_bound" )"1" "G(i!1)(x!1)" )"1" assert )"1" expand "abs" )"1" assert )nil nil ))nil ))nil )"2" "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" "2" "converges_upto_is_lub" "x" "SUP" "u" "lambda (n:nat): G(n)(x!1)" ))"2" "least_upper_bound?(SUP, LAMBDA (n:nat): G(n)(x!1), fullset[nat]))") "1" "1" expand "converges_upto?" )"1" expand "pointwise_increasing?" )"1" "x!1" )"1" replace "1" expand "pointwise_bounded_above?" )"1" expand "pointwise?" )"1" "x!1" )"1" assert )"1" "x!1" )"1" "x!1" )"1" "_" "x!1" )"1" "_" "x!1" )"1" "_" "x!1" )"1" "1" "convergence?(LAMBDA (n:nat): G(n)(x!1), f!1(x!1))" )"1" "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" "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" "1" expand "metric_converges_to" )"1" expand "ball" )"1" expand "member" )"1" "1" "r!1/2" )"1" "1" "n!1" )"1" "r!1/2" )"1" "1" "n!1+n!2" )"1" "1" "i!1" )"1" assert )"1" "n!1" )"1" assert )"1" "n!1" )"1" expand "abs" "1" assert )"1" "i!1" )"1" assert )"1" "i!1" )"1" assert )"1" case "forall (i:nat): ISF(n!1)(i)(x!1)<=F!1(n!1)(x!1)" )"1" "i!1" )"1" expand "abs" "1" assert )"1" case "ISF(n!1)(i!1)(x!1)<=G(i!1)(x!1)" )"1" assert )nil nil )"2" "2" expand "G" "2" "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" "i!1-n!1" )"1" assert )nil nil ))nil )"2" "2" "j" )"1" "n!1=0" )"1" expand "maximum" )"1" assert )nil nil ))nil )"2" expand "maximum" )"2" assert )"2" expand "max" )"2" nil nil ))nil ))nil ))nil ))nil )"2" "2" expand "maximum" "2" expand "max" )"2" "DRL1" "maximum(LAMBDA (i: nat): ISF(i)(i!1), n!1 + j!1)(x!1)" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "ISF" "2" "2" "choose({u: increasing_nn_isf | pointwise_convergence?(u, F!1(n!1))})" )"1" "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" "x!1" )"1" "x!1" )"1" rewrite "metric_convergence_def" )"1" expand "metric_converges_to" )"1" "DRL(i!2)(x!1) - F!1(n!1)(x!1)" )"1" "1" expand "ball" )"1" expand "member" )"1" "i!2+n!3" )"1" assert )"1" expand "increasing?" )"1" "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" "2" expand "nonempty?" )"2" expand "empty?" )"2" expand "member" )"2" "F!1(n!1)" )"2" expand "nn_integrable?" )"2" "2" "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" "2" "2" "n!1" )"2" "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" "2" expand "fullset" )"2" expand "image" )"2" expand "least_upper_bound?" )"2" expand "least_upper_bound" )"2" "2" "1" "1" expand "upper_bound" )"1" expand "upper_bound?" )"1" nil nil ))nil ))nil ))nil )"2" "2" "2" "y!1" )"2" "1" nil nil )"2" assert )nil nil )"3" "3" expand "upper_bound?" )"3" expand "upper_bound" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "Im" )"2" expand "pointwise_bounded_above?" )"2" expand "pointwise?" )"2" "x!1" )"2" expand "bounded_above?" )"2" expand "above_bounded" )"2" "2" expand "upper_bound" )"2" "ceiling(a!1)" )"2" "2" "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 ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "pointwise_bounded_above?" )"2" expand "pointwise?" )"2" "2" expand "bounded_above?" )"2" "f!1(x!1)" )"2" "2" "x!2" "x!1" )"2" "x!2" "x!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "nonempty?" )"2" expand "empty?" )"2" "G(0)" )"1" expand "member" )"1" (inst + "0" ) nil nil ))nil )"2" expand "nn_isf?" )"2" "2" "0" "x!1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "pointwise_increasing?" )"2" "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 (i: nat): ISF(i)(k), i+n)(x!1)" )"1" "1" "x!2" "x!2" "y!1" "y!1-x!2" )"1" (assert ) nil nil )"2" (assert ) nil nil ))nil ))nil )"2" "2" "n" )"1" "i" )"1" "1" expand "maximum" )"1" "0" )"1" expand "increasing_nn_isf?" )"1" expand "pointwise_increasing?" )"1" "x!1" )"1" expand "increasing?" )"1" "j!1" "k!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" expand "maximum" "2" expand "max" )"2" "j!2" "k!1" )"2" assert )"2" "DRL1" "maximum(LAMBDA (i: nat): ISF(i)(j!2), j!1)(x!1)" )"2" "DRL2" "maximum(LAMBDA (i: nat): ISF(i)(k!1), j!1)(x!1)" )"2" "1+j!1" )"2" expand "increasing_nn_isf?" )"2" expand "pointwise_increasing?" )"2" "x!1" )"2" expand "increasing?" )"2" "j!2" "k!1" )"2" assert )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "i" )"1" "1" expand "maximum" "1" expand "max" )"1" "0" "j!2" "k!1" )"1" assert )"1" "DRL1" "maximum(LAMBDA (i: nat): ISF(i)(k!1), j!1)(x!1)" )"1" expand "maximum" )"1" "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "maximum" "2" expand "max" )"2" "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)" )"1" "j!1" )"1" "DRL1" "maximum(LAMBDA (i: nat): ISF(i)(k!1), 1 + j!1 + j!2)(x!1)" )"1" "DRL2" "maximum(LAMBDA (i: nat): ISF(i)(j!3), j!2)(x!1)" )"1" "1" nil nil ))nil ))nil ))nil ))nil )"2" "2" "n" )"1" expand "maximum" )"1" expand "max" )"1" "1+j!2" )"1" expand "increasing_nn_isf?" )"1" expand "pointwise_increasing?" )"1" "x!1" )"1" expand "increasing?" )"1" "j!3" "k!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "maximum" "2" expand "max" )"2" "DRL1" "maximum(LAMBDA (i: nat): ISF(i)(k!1), 1 + j!4 + j!2)(x!1)" )"2" "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 )"2" (hide 2)"2" "2" expand "G" )"2" case "FORALL (n,j:nat,x:T): 0 <= maximum(LAMBDA (i: nat): ISF(i)(j), n)(x)" )"1" "1" "n!1" "n!1" "x!1" )nil nil ))nil )"2" "2" "_" "j!1" "x!1" ))"2" "n" )"1" expand "maximum" )"1" "ISF(0)(j!1)" )"1" expand "nn_isf?" )"1" "x!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" expand "maximum" 1)"2" expand "max" )"2" "ISF(1+j!2)(j!1)" )"2" expand "nn_isf?" )"2" "x!1" )"2" expand "max" )"2" "ISF(1 + j!2)(j!1)(x!1) < 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" "2" "x!1" )"2" "x!1" )"2" expand "increasing?" )"2" rewrite "metric_convergence_def" )"2" expand "metric_converges_to" )"2" "F!1(n!1)(x!1)-f!1(x!1)" )"1" "1" "n!1+n!2" )"1" expand "ball" )"1" expand "member" )"1" "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" "1" "n!1" "n!1" "x!1" )nil nil ))nil )"2" "2" "n" )"1" "1" expand "maximum" )"1" "0" )"1" "0" )"1" "1" expand "increasing_nn_isf?" )"1" expand "pointwise_convergence?" )"1" expand "pointwise_increasing?" )"1" "x!1" )"1" "x!1" )"1" rewrite "metric_convergence_def" )"1" expand "metric_converges_to" )"1" "ISF(0)(k!1)(x!1) - F!1(0)(x!1)" )"1" "1" expand "ball" )"1" expand "member" )"1" expand "abs" )"1" "n!1+k!1" )"1" assert )"1" expand "increasing?" )"1" "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" "2" expand "maximum" 1)"2" expand "max" )"2" "k!1" "x!1" )"2" "MAXI" "maximum(LAMBDA (i: nat): ISF(i)(k!1), j!1)(x!1)" )"2" expand "pointwise_increasing?" )"2" "x!1" )"2" expand "increasing?" )"2" "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" "ISF(1 + j!1)(k!1)(x!1) < MAXI" )"1" assert )nil nil )"2" assert )nil nil ))nil ))nil )"2" "2" "1+j!1" )"2" "1+j!1" )"2" expand "increasing_nn_isf?" )"2" expand "pointwise_convergence?" )"2" expand "pointwise_increasing?" )"2" "x!1" )"2" "x!1" )"2" rewrite "metric_convergence_def" )"2" expand "metric_converges_to" )"2" "ISF(1 + j!1)(k!1)(x!1) - F!1(1 + j!1)(x!1)" )"1" "1" expand "ball" )"1" expand "member" )"1" "n!1+k!1" )"1" expand "increasing?" )"1" "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" "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 )nil measure_space nil )"bool" measure_space_def nil )nil measure_space_defnil )"(p)" sets nil )"bool" sets nil )set type-eq-decl nil sets nil )nil nn_integral nil )"bool" nn_integral nil )nil nn_integral nil )"bool" nn_integral nil )nil isf nil )"bool" isf nil )"isf[T, S, m]" nil )"[T -> real]" real_fun_ops_aux "reals/" )"real" reals nil )"T" integral_convergence_scaf nil )"nat" integral_convergence_scaf nil )"nat" integral_convergence_scaf nil )"nat" integral_convergence_scaf nil )"T" integral_convergence_scaf nil )"bool" pointwise_convergencenil )nil integers nil )"bool" reals nil )"{i | x <= i & i < x + 1}" floor_ceil nil )"bool" bound_defs "reals/" )"T" integral_convergence_scaf nil )"nat" integral_convergence_scaf nil )nil convergence_aux"metric_space/" )"bool" bounded_real_defs nil )"bool" pointwise_convergence nil )"nonneg_int" nil )"[numfield, numfield -> numfield]" number_fields nil )"[n: nat -> ({u: increasing_nn_isf | pointwise_convergence?(u, F!1(n))})]" nil )"nat" integral_convergence_scaf nil )"({u: increasing_nn_isf | pointwise_convergence?(u, F!1(n!1))})" nil )"nat" integral_convergence_scaf nil )"sequence[nn_integrable]" nil )"posint" nil )"isf[T, S, m]" nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )max const-decl "[T -> real]" real_fun_ops_aux "reals/" )nil naturalnumbers nil )"int" integers nil )"int" integers nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"posreal" nil )nil hausdorff_convergence "topology/" )"bool" bounded_real_defs nil )"set[R]" function_image nil )"set" sets nil )"setof[real]" real_fun_props "reals/" )"{x | least_upper_bound(<=)(x, Su)}" bounded_reals"reals/" )nil bounded_reals "reals/" )"bool" bounded_reals "reals/" )"bool" bound_defs "reals/" )nil defined_types nil )"(nonempty?[real])" "extended_nnreal/" )"bool" sets nil )nil nn_integral nil )nil isf nil )nil nn_integral nil )"[nat -> isf[T, S, m]]" nil )"T" topological_convergence "topology/" )nil topological_convergence "topology/" )"bool" topological_convergence "topology/" )nil hausdorff_convergence "topology/" )"real" isf nil )NOT const-decl "[bool -> bool]" booleans nil )nil nn_integral nil )nil nn_integral nil )"bool" topological_convergence"topology/" )"setofsets[T]" metric_space_def"metric_space/" )"(hausdorff?)" "metric_space/" )"hausdorff[real]" "metric_space/" )"second_countable" real_topology "metric_space/" )"bool" convergence_aux"metric_space/" )nil isf nil )nil convergence_aux"metric_space/" )"nat" integral_convergence_scaf nil )"nat" integral_convergence_scaf nil )"odd_int" integersnil )"posint" nil )"nat" integral_convergence_scaf nil )"T" integral_convergence_scaf nil )"[T -> nnreal]" integral_convergence_scafnil )"bool" reals nil )"(strict_total_order?[real])" real_props nil )"T" integral_convergence_scaf nil )nil integral nil )nil integral nil )nil integral 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 )nil real_types nil )"real" integral nil )nil metric_space"metric_space/" )nil integral nil )"bool" pointwise_convergence nil )"bool" real_fun_preds "reals/" )"(total_order?[real])" nil )nil integral nil )"bool" metric_space_def"metric_space/" )nil real_types nil )"bool" reals nil )"set[T]" metric_space_def "metric_space/" )"bool" sets nil )"(total_order?[real])" nil )"metric_open[real, (LAMBDA (x, y: real): abs(x - y))]" "metric_space/" )"real" reals nil )nil integral nil )"[T, T -> boolean]" equalities nil )"[T -> real]" real_fun_ops "reals/" )"(strict_total_order?[real])" real_props nil )"bool" pointwise_convergencenil )"bool" real_fun_preds "reals/" )"bool" real_fun_preds "reals/" )"[T -> real]" integral_convergence_scaf nil )"sequence[integrable]" nil )nil integral nil )"bool" integral nil )"[T -> real]" real_fun_ops "reals/" )"integrable" 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 integral_convergence_scaf nil )nil real_types nil )nil defined_types nil )nil sets nil )"bool" subset_algebra_def nil )nil subset_algebra_def nil )"sigma_algebra" integral_convergence_scaf nil )nil extended_nnreal"extended_nnreal/" )"bool" generalized_measure_def nil )nil generalized_measure_defnil )"measure_type" integral_convergence_scaf nil )"bool" nn_integral nil )nil nn_integral nil )nil sequences nil )"[bool, bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" pointwise_convergencenil )"bool" real_fun_preds "reals/" )"T3" function_props nil )"nnreal" nn_integral nil )"bool" convergence_aux"metric_space/" ))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.309Angebot
(Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können 2026-04-27)
¤ *Eine klare Vorstellung vom Zielzustand
2026-05-26
