Impressum measure_contraction.prf
Sprache: Lisp
(measure_contractionnil 3431406180"" (skosimp)"" (assert )"" (lemma "measurable_intersection[T,S]" )"" (inst - "A!1" "E!1" )"" (expand "measurable_set?" ) (("" (propax) nil nil )) nil ))nil ))nil ))nil ))nil )"measurable_set" nil )set type-eq-decl nil sets nil )"bool" measure_space_def nil )nil measure_space_def nil )nil measure_space_def nil )nil measure_contraction nil )nil booleans nil )nil booleans nil )nil defined_types nil )nil sets nil )"bool" subset_algebra_def nil )nil subset_algebra_def nil )"sigma_algebra" measure_contraction nil ))nil ))nil 3431406180"" (expand "measurable_set?" ) (("" (propax) nil nil )) nil )"bool" measure_space_def nil )) nil ))nil 3431406180"" (skosimp)"" (typepred "mu!1" )"" (expand "measure?" )"" (flatten)"" (split)"1" (expand "measure_empty?" )"1" "intersection[T](A!1, emptyset[T])=emptyset[T]" )"1" (hide-all-but 1)"1" (apply-extensionality :hide? t)"1" (grind) nil nil )) nil ))nil ))nil ))nil )"2" (expand "measure_countably_additive?" )"2" (skosimp)"2" "lambda (n:nat): intersection[T](A!1, X!1(n))" )"1" (expand "o" )"1" "LHS" "x_sum(LAMBDA (x: nat): mu!1(intersection[T](A!1, X!1(x))))" )"1" "IUnion(LAMBDA (n: nat): intersection[T](A!1, X!1(n)))=intersection[T](A!1, IUnion(X!1))" )"1" (hide -1)"1" (assert )"1" (hide 1 -2)"1" "measurable_intersection[T,S]" "a" "A!1" "b" "IUnion(X!1)" ))"1" expand "measurable_set?" )"1" "IUnion(LAMBDA (n: nat): intersection[T](A!1, X!1(n)))=intersection[T](A!1, IUnion(X!1))" )"1" "1" "1" expand "intersection" )"1" expand "IUnion" )"1" expand "member" )"1" "A!1(x!1)" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "measurable_set?" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (skosimp)"2" "measurable_intersection[T,S]" "a" "A!1" "b" "X!1(x!1)" ))"1" (expand "measurable_set?" )"1" (propax) nil nil )) nil )"2" (expand "measurable_set?" )"2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (typepred "X!1" )"2" (expand "disjoint_indexed_measurable?" )"2" (expand "disjoint?" )"2" (expand "disjoint?" )"2" (expand "intersection" )"2" expand "empty?" )"2" expand "member" )"2" "2" "2" "i!1" "j!1" )"2" assert )"2" "x!1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide-all-but 1)"3" (skosimp)"3" "measurable_intersection[T,S]" "a" "A!1" "b" "X!1(n!1)" ))"1" (expand "measurable_set?" )"1" (propax) nil nil )) nil )"2" (expand "measurable_set?" )"2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil generalized_measure_defnil )"bool" generalized_measure_def nil )nil extended_nnreal"extended_nnreal/" )nil real_types nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )"sigma_algebra" measure_contraction nil )nil subset_algebra_def nil )"bool" subset_algebra_def nil )nil sets nil )nil defined_types nil )nil measure_contraction nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"(S)" nil )"bool" nil )"disjoint_indexed_measurable[T, S]" nil )nil nil )"bool" nil )"measurable_set[T, S]" measure_contractionnil )nil naturalnumbers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"extended_nnreal" extended_nnreal"extended_nnreal/" )nil measure_space_def nil )"set[T]" indexed_sets nil )"T3" function_props nil )"bool" indexed_sets_aux "sets_aux/" )"bool" sets nil )"bool" sets nil )"(S)" nil )"bool" generalized_measure_def nil )"bool" sets nil )"(S)" measure_contractionnil )"measurable_set" nil )"finite_set[T]" countable_setofsets"sets_aux/" )"finite_set[T]" countable_props"sets_aux/" )"finite_set" finite_sets nil )"finite_set[T]" "sets_aux/" )"countable_set[T]" "sets_aux/" )"measurable_set" nil )set type-eq-decl nil sets nil )"[T, T -> boolean]" equalities nil )"set" sets nil )"bool" measure_space_def nil )nil measure_space_def nil )"set" sets nil ))nil ))nil 3456294370 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil measure_contraction nil )set type-eq-decl nil sets nil )nil defined_types nil )nil sets nil )"bool" subset_algebra_def nil )nil subset_algebra_def nil )"sigma_algebra" measure_contraction nil )"bool" measure_space_def nil )nil measure_space_def nil ))nil ))nil 3456294370"" (skosimp)"" (lemma "contraction_TCC3" ("mu" "mu!1" "A" "A!1" ))"" (typepred "A!1" )"" (typepred "mu!1" )"" (lemma "measure_monotone" ("f" "mu!1" "b" "A!1" ))"" (replace -2)"" (expand "x_le" )"" (expand "finite_measure?" )"" (expand "measure?" -5)"" (hide -2)"" (flatten)"" (split)"1" (expand "measure_empty?" )"1" (replace -4) (("1" (assert ) nil nil ))nil ))nil )"2" (skosimp)"2" (typepred "X!1" )"2" expand "measure_countably_additive?" )"2" "X!1" )"2" expand "o " )"2" expand "x_eq" )"2" "2" "2" "intersection[T](A!1, IUnion(X!1))" )"2" "1" "1" replace -1)"1" replace -7)"1" replace -8 1 rl)"1" "1" expand "x_sum" )"1" "FORALL (i:nat): mu!1(intersection[T](A!1, X!1(i)))`1" )"1" "1" "1" rewrite "limit_lemma" )"1" "1" "i!1" )"1" "measurable_intersection" "a" "A!1" "b" "X!1(i!1)" ))"1" expand "measurable_set?" )"1" nil nil ))nil )"2" expand "measurable_set?" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace "2" nil nil ))nil )"3" "3" "3" expand "disjoint_indexed_measurable?" )"3" expand "measurable_set?" )"3" "measurable_intersection" "a" "A!1" "b" "X!1(i!1)" ))"1" assert )"1" expand "measurable_set?" )"1" nil nil ))nil ))nil )"2" expand "measurable_set?" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))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 ))nil ))nil ))nil ))nil ))nil )nil measure_space_def nil )"bool" measure_space_def nil )set type-eq-decl nil sets nil )nil generalized_measure_defnil )"bool" generalized_measure_def nil )nil extended_nnreal"extended_nnreal/" )nil real_types nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )"sigma_algebra" measure_contraction nil )nil subset_algebra_def nil )"bool" subset_algebra_def nil )nil sets nil )nil defined_types nil )nil booleans nil )nil booleans nil )nil measure_contraction nil )nil measure_contraction nil )"(S)" nil )"bool" generalized_measure_def nil )"bool" generalized_measure_def nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )"bool" nil )nil nil )"bool" extended_nnreal "extended_nnreal/" )"extended_nnreal" extended_nnreal"extended_nnreal/" )"sequence[real]" series "series/" )"bool" convergence_sequences "analysis/" )nil sequences nil )nil convergence_sequences "analysis/" )"(total_order?[real])" nil )nil measure_space_def nil )"(partial_order?[set[T]])" nil )"bool" sets nil )"bool" sets nil )"set" sets nil )"set[T]" indexed_sets nil )"T3" function_props nil )"bool" nil )"bool" extended_nnreal "extended_nnreal/" )nil measure_def nil )NOT const-decl "[bool -> bool]" booleans nil ))nil ))nil 3457156931"" (skosimp)"" (expand "measurable_set?" )"" (lemma "A_of_TCC1" ("f" "nu!1" ))"" "choose_member" "a" "{X: disjoint_indexed_measurable[T, S] | AND (FORALL i: nu!1(X(i))`1)}")) "" (split)"1" (expand "member" )"1" (flatten)"1" (inst - "i!1" )"1" (expand "A_of" ) (("1" (propax) nil nil )) nil ))nil ))nil ))nil )"2" (expand "nonempty?" ) (("2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"bool" measure_space_def nil )nil nil )"bool" nil )nil naturalnumbers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"set" sets nil )"set[T]" indexed_sets nil )"[T, T -> boolean]" equalities nil )AND const-decl "[bool, bool -> bool]" booleans nil )set type-eq-decl nil sets nil )nil sets_lemmas nil )"(S)" nil )"bool" sets nil )"bool" sets nil )"disjoint_indexed_measurable" measure_def nil )nil measure_def nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil real_types nil )nil extended_nnreal"extended_nnreal/" )"bool" measure_def nil )nil measure_def nil )nil measure_contraction nil )nil booleans nil )nil booleans nil )nil defined_types nil )nil sets nil )"bool" subset_algebra_def nil )nil subset_algebra_def nil )"sigma_algebra" measure_contraction nil ))nil ))nil 3457156932"" (skosimp)"" (typepred "nu!1" )"" (expand "sigma_finite_measure?" )"" (expand "measure?" )"" (flatten)"" (expand "measure_countably_additive?" )"" (inst - "lambda i: intersection(A_of(nu!1)(i),E!1)" )"1" (name "AA" "A_of(nu!1)" )"1" (replace -1)"1" (expand "fm_contraction" )"1" (expand "o " )"1" (expand "A_of" )"1" (lemma "A_of_TCC1" ("f" "nu!1" ))"1" "choose_member" "a" "{X: disjoint_indexed_measurable[T, S] | AND (FORALL i: nu!1(X(i))`1)}")) "1" "1" replace -3)"1" expand "member" )"1" "1" "1" "IUnion(LAMBDA i: intersection(AA(i), E!1))=E!1" )"1" "1" "x_sum_eq" "S" "LAMBDA i: nu!1(intersection(AA(i), E!1))" "T" "LAMBDA i: (TRUE, nu!1(intersection(AA(i), E!1))`2)" ))"1" "1" expand "x_eq" )"1" "1" replace -1 * rl)"1" assert )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" "i!1" )"2" "measure_monotone" "f" "nu!1" "a" "intersection(AA(i!1), E!1)" "b" "AA(i!1)" ))"2" "1" expand "x_le" )"1" assert )"1" "1" expand "x_eq" )"1" nil nil ))nil ))nil ))nil ))nil )"2" assert )"2" "nu!1" )"2" expand "sigma_finite_measure?" )"2" nil nil ))nil ))nil ))nil )"3" "3" expand "intersection" )"3" expand "subset?" )"3" expand "member" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "measurable_intersection" "a" "AA(i!1)" "b" "E!1" ))"1" expand "measurable_set?" )"1" nil nil ))nil )"2" expand "measurable_set?" )"2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "extensionality_postulate" "f" "IUnion[nat, T](AA)" "g" "fullset[T]" ))"2" "2" "1" "1" "x!1" )"1" expand "fullset" )"1" expand "IUnion" )"1" "1" "E!1(x!1)" )"1" expand "intersection" )"1" expand "member" )"1" "i!1" )"1" assert )nil nil ))nil ))nil ))nil )"2" assert )"2" "2" expand "intersection" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "nonempty?" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (typepred "A_of[T, S](nu!1)" )"2" (expand "disjoint_indexed_measurable?" )"2" (expand "disjoint?" )"2" (skosimp)"2" (inst - "i!1" "j!1" )"2" (assert )"2" expand "disjoint?" )"2" expand "intersection" )"2" expand "empty?" )"2" expand "member" )"2" "2" "x!1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (skosimp)"3" "measurable_intersection" "a" "A_of[T, S](nu!1)(i!1)" "b" "E!1" ))"1" (expand "measurable_set?" )"1" (propax) nil nil )) nil )"2" (expand "measurable_set?" )"2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil measure_def nil )"bool" measure_def nil )nil extended_nnreal"extended_nnreal/" )nil real_types nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )"sigma_algebra" measure_contraction nil )nil subset_algebra_def nil )"bool" subset_algebra_def nil )nil sets nil )nil defined_types nil )nil measure_contraction nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"bool" generalized_measure_def nil )"(S)" nil )"bool" nil )"bool" sets nil )"bool" sets nil )"bool" indexed_sets_aux "sets_aux/" )"[T, T -> boolean]" equalities nil )"finite_measure" measure_contractionnil )nil sets_lemmas nil )AND const-decl "[bool, bool -> bool]" booleans nil )"set[T]" indexed_sets nil )"set" sets nil )"bool" sets nil )nil extended_nnreal "extended_nnreal/" )"bool" booleans nil )nil measure_def nil )"bool" sets nil )"bool" extended_nnreal "extended_nnreal/" )"(total_order?[real])" nil )"bool" extended_nnreal "extended_nnreal/" )"measurable_set[T, S]" nil )"(S)" measure_contractionnil )nil measure_space_def nil )nil functions nil )"bool" sets nil )nil measure_def nil )"T3" function_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 )"set" sets nil )"bool" nil )nil nil )"disjoint_indexed_measurable" measure_def nil )"sigma_finite_measure[T, S]" nil )"bool" measure_space_def nil )nil measure_space_def nil )"measurable_set[T, S]" measure_contractionnil ))nil 3460361064"" (skosimp)"" (typepred "nu!1" )"" (expand "sigma_finite_measure?" )"" (flatten)"" (expand "measure_sigma_finite?" )"" (skosimp)"" (inst + "X!1" )"" (replace -2)"" (skosimp)"" (inst - "i!1" )"" (expand "contraction" )"" "m_monotone[T,S,nu!1]" "a" "intersection(A!1, X!1(i!1))" "b" "X!1(i!1)" ))"1" (expand "x_le" )"1" (assert )"1" "1" expand "intersection" )"1" expand "subset?" )"1" expand "member" )"1" (skosimp) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "measurable_set?" )"2" (propax) nil nil )) nil )"3" (expand "measurable_set?" )"3" (typepred "A!1" )"3" "X!1(i!1)" )"3" "measurable_intersection" "a" "A!1" "b" "X!1(i!1)" ))"1" expand "measurable_set?" )"1" (propax) nil nil ))nil )"2" expand "measurable_set?" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil measure_def nil )"bool" measure_def nil )nil extended_nnreal"extended_nnreal/" )nil real_types nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )"sigma_algebra" measure_contraction nil )nil subset_algebra_def nil )"bool" subset_algebra_def nil )nil sets nil )nil defined_types nil )nil measure_contraction nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"set" sets nil )nil measure_space_def nil )"bool" measure_space_def nil )set type-eq-decl nil sets nil )nil measure_props nil )"(partial_order?[set[T]])" nil )"(S)" measure_contractionnil )"measurable_set[T, S]" nil )"(S)" nil )"bool" sets nil )"bool" sets nil )"bool" extended_nnreal "extended_nnreal/" )nil measure_space_def nil )"measure_type" measure_contraction nil )nil nil )"bool" nil )nil naturalnumbers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"bool" measure_def nil ))nil ))nil 3431719231"" (skosimp)"" (split)"1" (flatten)"1" (expand "isf?" )"1" (split)"1" (lemma "phi_is_simple[T,S]" ("X" "A!1" ))"1" (lemma "simple_times" ("h1" "phi(A!1)" "h2" "f!1" ))"1" (propax) nil nil ) ("2" (propax) nil nil )) nil )"2" (typepred "A!1" )"2" (expand "measurable_set?" )"2" (propax) nil nil )) nil ))nil ))nil )"2" (expand "mu_fin?" )"2" (expand "contraction" )"2" (expand "nonzero_set?" )"2" (expand "intersection" )"2" (expand "phi" )"2" (expand "member" )"2" (expand "*" )"2" "{x: T | IF A!1(x) THEN 1 ELSE 0 ENDIF * f!1(x) /= 0}={x_1: T | A!1(x_1) AND f!1(x_1) /= 0}" )"2" (hide -1 2)"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" (expand "isf?" )"2" (flatten)"2" (hide -1)"2" (expand "nonzero_set?" )"2" (expand "mu_fin?" )"2" (expand "contraction" )"2" (expand "intersection" )"2" (expand "phi" )"2" (expand "member" )"2" (expand "*" )"2" "{x: T | IF A!1(x) THEN 1 ELSE 0 ENDIF * f!1(x) /= 0}={x_1: T | A!1(x_1) AND f!1(x_1) /= 0}" )"2" "2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" isf nil )"bool" measure_props nil )"set[T]" isf nil )"[T -> real]" real_fun_ops "reals/" )"real" reals nil )"nonneg_int" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )AND const-decl "[bool, bool -> bool]" booleans nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )"[T, T -> boolean]" equalities nil )"real" reals nil )"bool" sets nil )"set" sets nil )"measure_type" measure_contraction nil )"sigma_algebra" measure_contraction nil )nil subset_algebra_def nil )"bool" subset_algebra_def nil )nil sets nil )nil defined_types nil )nil booleans nil )nil booleans nil )nil measure_contraction nil )nil measure_space_def nil )"bool" measure_space_def nil )set type-eq-decl nil sets nil )nil measure_space nil )nil measure_space nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" measure_space nil )nil measure_space nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"nat" measure_space nil )NOT const-decl "[bool -> bool]" booleans nil ))nil 3431698665"" (skosimp)"" (typepred "f!1" )"" (rewrite "contraction_isf" )"" (expand "isf?" )"" (expand "simple?" ) (("" (propax) nil nil )) nil )) nil ))nil ))nil ))nil )nil isf nil )"bool" isf nil )"measure_type" measure_contraction nil )nil measure_space_def nil )"bool" measure_space_def nil )set type-eq-decl nil sets nil )nil generalized_measure_defnil )"bool" generalized_measure_def nil )nil extended_nnreal"extended_nnreal/" )nil real_types nil )"bool" reals nil )"sigma_algebra" measure_contraction nil )nil subset_algebra_def nil )"bool" subset_algebra_def nil )nil sets nil )nil defined_types nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil measure_contraction nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil measure_space nil )"bool" measure_space nil )nil measure_contraction nil ))nil ))nil 3431720982"" (skosimp)"" (typepred "f!1" )"" (lemma "contraction_isf" ("mu" "mu!1" "A" "A!1" "f" "f!1" ))"" (assert )"" (expand "isf_integral" )"" (expand "mu" )"" (expand "contraction" )"" case "FORALL (c: real): NOT c = 0 IMPLIES") "1" "(LAMBDA (c:real): IF c = 0 THEN 0LAMBDA (c:real):IF c = 0 THEN 0") "1" (hide -1)"1" "F" "LAMBDA(c: real):IF c = 0 THEN 0 ") "1" (replace -1)"1" (expand "isf?" )"1" (expand "simple?" )"1" "1" "1" "sigma_add[real]" "f" "F" "X" "image[T, real](f!1, fullset[T])" "t" "0" ))"1" expand "F" -1 3)"1" replace -1 1 rl)"1" case "subset?[real](image[T, real] ") "1" "sigma_subset[real]" "X" "image[T, real] " "Y" "add[real](0, image[T, real](f!1, fullset[T]))" "f" "F" ))"1" replace -2)"1" replace -1)"1" "1" assert )"1" "sigma_eq[real]" "X" "difference[real](add[real](0, image[T, real](f!1, fullset[T])), ")) "1" "F" "lambda (c:real): 0" )"1" "1" replace "1" rewrite "sigma_zero[real]" nil nil ))nil )"2" "2" "2" "t!1" )"2" "2" expand "difference" )"2" expand "member" )"2" "2" expand "add" )"2" expand "F" )"2" expand "inverse_image" )"2" expand "member" )"2" expand "singleton" )"2" expand "*" )"2" "1" replace "1" nil nil ))nil )"2" "t!1=0" )"2" assert )"2" "{x: T | phi[T, S](A!1)(x) * f!1(x) = t!1}=emptyset[T]" )"1" "mu!1" )"1" expand "measure?" )"1" "1" expand "measure_empty?" )"1" replace "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "emptyset" )"2" "2" expand "fullset" )"2" expand "image" )"2" "x!1" )"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 )"2" "2" expand "convergent?" )"2" "2" "2" rewrite "finite_difference" )"2" rewrite "finite_add" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "subset?" )"2" expand "add" )"2" expand "fullset" )"2" expand "*" )"2" expand "phi" )"2" expand "image" )"2" expand "member" )"2" "2" "A!1(x!2)" )"1" "x!2" )"1" assert )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 )"2" (propax) nil nil ))nil ))nil )"2" (hide 2)"2" (apply-extensionality :hide? t)"1" (case-replace "x!1=0" )"1" (assert )"1" "inverse_image[T, real] ") "1" "1" "1" (grind) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp)"2" (inst - "c!1" )"2" (assert )"2" "inverse_image[T, real] ") "2" "2" "2" expand "inverse_image" )"2" expand "intersection" )"2" expand "phi" )"2" expand "*" )"2" expand "member" )"2" expand "singleton" )"2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide 2)"3" (skosimp)"3" (inst - "c!1" )"3" (assert )"3" "inverse_image[T, real] ") "3" "3" "3" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skosimp)"2" "prod_measurable[T,S]" "g1" "phi[T, S](A!1)" "g2" "f!1" ))"1" (expand "measurable_function?" )"1" (inst - "singleton[real](c!1)" )"1" (expand "measurable_set?" )"1" (propax) nil nil )) nil )"2" (lemma "singleton_is_borel" )"2" (inst - "c!1" ) nil nil )) nil ))nil ))nil )"2" (lemma "phi_is_simple[T,S]" ("X" "A!1" ))"1" (expand "simple?" )"1" (flatten) nil nil )) nil )"2" (typepred "A!1" )"2" (expand "measurable_set?" )"2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil isf nil )"bool" isf nil )"measure_type" measure_contraction nil )nil measure_space_def nil )"bool" measure_space_def nil )set type-eq-decl nil sets nil )nil generalized_measure_defnil )"bool" generalized_measure_def nil )nil extended_nnreal"extended_nnreal/" )nil real_types nil )"bool" reals nil )"sigma_algebra" measure_contraction nil )nil subset_algebra_def nil )"bool" subset_algebra_def nil )nil sets nil )nil defined_types nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil measure_contraction nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"nnreal" measure_props nil )"(singleton?)" sets nil )"bool" sets nil )"nat" measure_space nil )nil naturalnumbers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"[T -> real]" real_fun_ops "reals/" )"set[D]" function_image nil )"[T, T -> boolean]" equalities nil )"[bool, bool -> bool]" booleans nil )"real" reals nil )"non_empty_finite_set[real]" measure_space nil )"compact[real, (metric_induced_topology)]" convergence_aux"metric_space/" )"closed[real, (metric_induced_topology)]" convergence_aux"metric_space/" )"[real -> real]" measure_contraction nil )"bool" sets nil )"bool" sets nil )"(nonempty?)" sets nil )nil sigma_countable "sigma_set/" )"set" sets nil )nil finite_sets nil )"bool" finite_sets nil )nil finite_sets nil )nil finite_sets nil )nil sigma_countable "sigma_set/" )"bool" sets nil )"bool" booleans nil )"bool" generalized_measure_def nil )"finite_set" finite_sets nil )"finite_set[T]" countable_props"sets_aux/" )"finite_set[T]" countable_setofsets"sets_aux/" )"finite_set[T]" sigma_countable"sigma_set/" )"measurable_set" nil )"(S)" measure_contractionnil )"set" sets nil )"isf[T, S, contraction(mu!1, A!1)]" nil )"measurable_set[T, S]" measure_contractionnil )"measure_type[T, S]" measure_contractionnil )"(partial_order?[set[T]])" nil )"measurable_set[T, S]" nil )"(S)" measure_contractionnil )"real" reals nil )nil sigma_countable "sigma_set/" )"bool" countable_convergence "sigma_set/" )"set" sets nil )"set[R]" function_image nil )nil countability "sets_aux/" )"bool" countability "sets_aux/" )nil sigma_countable "sigma_set/" )"real" reals nil )nil number_fields nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"[numfield, numfield -> numfield]" number_fields nil )"set" sets nil )nil measure_space nil )nil real_types nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield, numfield -> numfield]" number_fields nil )"setofsets[T]" metric_space_def"metric_space/" )"sigma_algebra" borel nil )nil borel nil )nil measure_space_defnil )"bool" measure_space_def nil )nil measure_space nil )"real" isf nil )nil measure_contraction nil )"bool" measure_space nil )nil measure_space nil ))nil 3431698665"" (skosimp)"" (skosimp)"" (typepred "f!1" )"" (expand "nn_measurable?" )"" (flatten)"" (inst - "x1!1" ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )"(total_order?[real])" nil )"(total_order?[real])" nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil measure_contraction nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil defined_types nil )nil sets nil )"bool" subset_algebra_def nil )nil subset_algebra_def nil )"sigma_algebra" measure_contraction nil )"bool" measure_space nil )nil measure_space nil ))nil ))nil 3431698665"" (skosimp)"" (skosimp)"" (typepred "f!1" )"" (expand "nn_measurable?" )"" (flatten)"" (inst - "x1!1" )"" (hide -1) (("" (grind) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil )"real" reals nil )"real" reals nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"bool" sets nil )"nat" measure_space nil )"[T -> real]" real_fun_ops "reals/" )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil measure_contraction nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil defined_types nil )nil sets nil )"bool" subset_algebra_def nil )nil subset_algebra_def nil )"sigma_algebra" measure_contraction nil )"bool" measure_space nil )nil measure_space nil ))nil ))nil 3431698666"" (skosimp)"" (split)"1" (flatten)"1" (expand "nn_integrable?" )"1" (skosimp)"1" "lambda (n:nat): ((reals@real_fun_ops[T].*) ") "1" (split)"1" (expand "pointwise_convergence?" )"1" (skosimp)"1" (inst - "x!1" )"1" (expand "*" )"1" (expand "phi" )"1" (expand "member" )"1" (case-replace "A!1(x!1)" )"1" (assert ) nil nil )"2" assert )"2" "2" expand "convergence?" )"2" "2" "0" )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -1)"2" (expand "convergent?" )"2" (skosimp)"2" (inst + "l!1" )"2" (expand "o " )"2" "(LAMBDA (n: nat): isf_integral[T,S,contraction(mu!1,A!1)](u!1(n)))=(LAMBDA (n: nat): ") "1" (hide -1 2)"1" "1" rewrite "contraction_isf_integral" )nil nil )"2" "2" "u!1(n!1)" )"2" rewrite "contraction_isf" )"2" expand "isf?" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -1 2)"2" "2" "u!1(n!1)" )"2" "2" rewrite "contraction_isf" )"2" "2" expand "isf?" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (typepred "u!1" )"2" (hide -2 -3)"2" (expand "increasing_nn_isf?" )"2" (expand "pointwise_increasing?" )"2" (skosimp)"2" (inst - "x!1" )"2" (expand "increasing?" )"2" (skolem + ("i!1" "j!1" ))"2" "i!1" "j!1" )"2" "2" assert )"2" expand "*" )"2" expand "phi" )"2" expand "member" )"2" "A!1(x!1)" )"1" (assert ) nil nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (expand "nn_isf?" )"3" (skosimp)"3" (typepred "u!1(n!1)" )"3" (expand "nn_isf?" )"3" (split)"1" (rewrite "contraction_isf" )"1" (expand "isf?" )"1" (propax) nil nil )) nil ))nil )"2" (skosimp)"2" (inst - "x!1" )"2" (hide -1 -3 -4)"2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" (typepred "f!1" )"2" (lemma "nn_measurable_def" ("f" "f!1" ))"2" (expand "nn_measurable?" )"2" (flatten)"2" (replace -2)"2" (replace -3)"2" (assert )"2" (skosimp)"2" (expand "pointwise_converges_upto?" )"2" (flatten)"2" (expand "nn_integrable?" )"2" "2" "lambda (n:nat): ((reals@real_fun_ops[T].*) ") "1" "1" expand "pointwise_convergence?" )"1" "1" "x!1" )"1" "x!1" )"1" "1" expand "+" )"1" expand "*" )"1" expand "phi" )"1" expand "complement" )"1" expand "member" )"1" "A!1(x!1)" )"1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "convergent?" )"2" "2" "l!1" )"2" expand "o " )"2" case "FORALL (n: nat): ") "1" "(LAMBDA (n: nat): LAMBDA (n: nat): isf_integral[T,S,mu!1](u!1(n)))") "1" "1" "1" "x!1" )"1" rewrite "isf_integral_add[T, S, contraction(mu!1, A!1)]" )"1" "isf_integral[T,S,contraction(mu!1,A!1)](((((reals@real_fun_ops[T].*) ") "1" "1" "isf_integral[T, S, mu!1](u!1(x!1))=isf_integral[T, S, mu!1](((reals@real_fun_ops[T].*) ") "1" "1" "contraction_isf_integral" "mu" "mu!1" "A" "A!1" "f" "u!1(x!1)" ))"1" "(((reals@real_fun_ops[T].*)(phi[T, S](A!1), u!1(x!1))))=u!1(x!1)" )"1" "u!1(x!1)" )"1" "contraction_isf" "mu" "mu!1" "A" "A!1" "f" "u!1(x!1)" ))"1" replace "1" assert )nil nil ))nil )"2" expand "isf?" )"2" expand "simple?" )"2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "*" )"2" expand "pointwise_convergence?" )"2" "x!2" )"2" expand "phi" )"2" expand "member" )"2" "A!1(x!2)" )"1" assert )nil nil )"2" assert )"2" "u!1(x!1)" )"2" expand "nn_isf?" )"2" "x!2" )"2" expand ">=" "2" expand "<=" "2" "2" rewrite "metric_convergence_def" )"2" expand "metric_converges_to" )"2" "u!1(x!1)(x!2)" )"1" "1" expand "ball" )"1" expand "member" )"1" "max(n!1,x!1)" )"1" "1" "u!1(max(n!1, x!1))" )"1" expand "nn_isf?" )"1" "x!2" )"1" "abs(-1 * u!1(max(n!1, x!1))(x!2))=u!1(max(n!1, x!1))(x!2)" )"1" "1" "u!1" )"1" expand "increasing_nn_isf?" )"1" expand "pointwise_increasing?" )"1" "x!2" )"1" expand "increasing?" )"1" "x!1" "max(n!1, x!1)" )"1" "1" assert )nil nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" 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 )"2" "2" "u!1(x!1)" )"2" expand "isf?" )"2" "2" assert )"2" expand "mu_fin?" )"2" expand "contraction" )"2" "m_monotone[T,S,mu!1]" "a" "intersection(A!1, nonzero_set?(u!1(x!1)))" "b" "nonzero_set?(u!1(x!1))" ))"1" "1" expand "x_le" )"1" assert )"1" "1" assert )"1" expand "nonzero_set?" )"1" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "subset?" )"2" expand "intersection" )"2" expand "nonzero_set?" )"2" expand "member" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "nonzero_measurable[T, S, mu!1]" "g" "u!1(x!1)" ))"1" nil nil )"2" expand "simple?" )"2" nil nil ))nil ))nil )"3" "3" rewrite "measurable_intersection" )"3" "nonzero_measurable[T, S, mu!1]" "g" "u!1(x!1)" ))"1" nil nil )"2" expand "simple?" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "(((reals@real_fun_ops[T].*)(phi[T, S](A!1), u!1(x!1))))=u!1(x!1)" )"2" "2" expand "*" )"2" "2" expand "phi" )"2" expand "member" )"2" expand "pointwise_convergence?" )"2" "2" "x!2" )"2" rewrite "metric_convergence_def" )"2" expand "metric_converges_to" )"2" expand "member" )"2" expand "ball" )"2" "A!1(x!2)" )"1" assert )nil nil )"2" assert )"2" "u!1(x!1)(x!2)" )"1" "1" "u!1" )"1" expand "increasing_nn_isf?" )"1" expand "pointwise_increasing?" )"1" "x!2" )"1" expand "increasing?" )"1" "x!1" "max(n!1,x!1)" )"1" "1" "max(n!1, x!1)" )"1" "1" "abs(-1 * u!1(max(n!1, x!1))(x!2))=u!1(max(n!1, x!1))(x!2)" )"1" assert )nil nil )"2" "2" "u!1(max(n!1, x!1))" )"2" expand "nn_isf?" )"2" "x!2" )"2" expand "abs" )"2" assert )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "u!1(x!1)" )"2" expand "nn_isf?" )"2" "x!2" )"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 ))nil ))nil ))nil )"3" "3" "u!1(x!1)" )"3" "isf_times_simple_is_isf[T, S, mu!1]" "i" "u!1(x!1)" "h" "phi[T, S](A!1)" ))"1" "(((reals@real_fun_ops[T].*)(phi[T, S](A!1), u!1(x!1))))=*[T](u!1(x!1), phi[T, S](A!1))" )"1" "1" expand "*" )"1" expand "phi" )"1" expand "member" )"1" "A!1(x!2)" )"1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" rewrite "phi_is_simple" )"2" "A!1" )"2" expand "measurable_set?" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "isf_integral" )"2" expand "mu" )"2" expand "contraction" )"2" expand "intersection" )"2" expand "complement" )"2" expand "phi" )"2" expand "member" )"2" "(LAMBDA (c:real): IF c = 0 THEN 0AND LAMBDA IF NOT A!1(x_1) THEN 1 ELSE 0 ENDIF,LAMBDA (c:real):0)") "1" "1" rewrite "sigma_zero" nil nil ))nil )"2" "2" "1" "x!2 = 0" )"1" assert )"1" "{x: T | AND LAMBDA (x_1: T):IF NOT A!1(x_1) THEN 1 ELSE 0 ENDIF,") "1" "mu!1" )"1" expand "measure?" )"1" expand "measure_empty?" )"1" "1" replace "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "emptyset" )"2" "2" expand "inverse_image" )"2" expand "*" )"2" expand "member" )"2" assert )"2" expand "singleton" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "{x: T | AND LAMBDA (x_1: T):IF NOT A!1(x_1) THEN 1 ELSE 0 ENDIF,") "1" assert )nil nil )"2" "2" "2" expand "emptyset" )"2" "2" assert )"2" expand "inverse_image" )"2" expand "member" )"2" expand "*" )"2" expand "singleton" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "3" "3" "{x: T | AND LAMBDA (x_1: T):IF NOT A!1(x_1) THEN 1 ELSE 0 ENDIF,") "1" assert )nil nil )"2" "2" "2" expand "emptyset" )"2" "2" expand "inverse_image" )"2" expand "member" )"2" expand "*" )"2" assert )"2" expand "singleton" )"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 )"2" "2" "2" expand "isf?" )"2" "1" "w!1" )"1" expand "increasing_nn_simple?" )"1" "x!1" )"1" expand "nn_simple?" )"1" "1" rewrite "simple_times[T,S]" "1" "1" rewrite "phi_is_simple" )"1" "measurable_complement[T,S]" "a" "A!1" ))"1" expand "measurable_set?" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "nonzero_set?" )"2" expand "*" )"2" expand "complement" )"2" expand "mu_fin?" )"2" expand "contraction" )"2" expand "intersection" )"2" expand "phi" )"2" expand "member" )"2" "{x_1: T | AND IF NOT A!1(x_1) THEN 1 ELSE 0 ENDIF * w!1(x!1)(x_1) /= 0}=emptyset[T]") "1" "mu!1" )"1" expand "measure?" )"1" "1" expand "measure_empty?" )"1" replace "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "emptyset" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "u!1(x!1)" )"3" "isf_times_simple_is_isf[T, S, contraction(mu!1, A!1)]" "i" "u!1(x!1)" "h" "phi[T, S](A!1)" ))"1" "(*[T](u!1(x!1), phi[T, S](A!1)))=(((((reals@real_fun_ops[T].*)(phi[T, S](A!1), u!1(x!1))))))" )"1" "1" expand "*" )"1" expand "phi" )"1" expand "member" )"1" "A!1(x!2)" )"1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "isf?" )"2" expand "mu_fin?" )"2" "2" assert )"2" expand "contraction" )"2" "m_monotone[T,S,mu!1]" "a" "intersection(A!1, nonzero_set?(u!1(x!1)))" "b" "nonzero_set?(u!1(x!1))" ))"1" "1" expand "x_le" )"1" "1" assert )"1" expand "nonzero_set?" )"1" nil nil ))nil ))nil ))nil ))nil )"2" "2" expand "subset?" )"2" expand "intersection" )"2" expand "member" )"2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "nonzero_measurable[T,S,mu!1]" "g" "u!1(x!1)" ))"1" nil nil )"2" expand "simple?" )"2" nil nil ))nil ))nil )"3" rewrite "measurable_intersection[T,S]" "3" "nonzero_measurable[T,S,mu!1]" "g" "u!1(x!1)" ))"1" nil nil )"2" expand "simple?" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" rewrite "phi_is_simple[T, S]" )"3" "A!1" )"3" expand "measurable_set?" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" rewrite "isf_add[T, S, contraction(mu!1, A!1)]" "1" "1" expand "isf?" )"1" "1" rewrite "simple_times" "1" "w!1" )"1" expand "increasing_nn_simple?" )"1" "n!1" )"1" expand "nn_simple?" )"1" nil nil ))nil ))nil ))nil ))nil )"2" rewrite "phi_is_simple" "2" "measurable_complement[T,S]" "a" "A!1" ))"2" expand "measurable_set?" )"2" nil nil ))nil ))nil ))nil ))nil )"2" expand "nonzero_set?" )"2" expand "/=" )"2" expand "mu_fin?" )"2" expand "contraction" )"2" expand "intersection" )"2" expand "*" )"2" expand "complement" )"2" expand "phi" )"2" expand "member" )"2" "{x_1: T | AND NOT (IF NOT A!1(x_1) THEN 1 ELSE 0 ENDIF * w!1(n!1)(x_1) =") "1" "mu!1" )"1" expand "measure?" )"1" "1" expand "measure_empty?" )"1" replace "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "emptyset" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "isf_times_simple_is_isf[T, S, contraction(mu!1, A!1)]" "i" "u!1(n!1)" "h" "phi[T, S](A!1)" ))"1" "(*[T](u!1(n!1), phi[T, S](A!1)))=(((((reals@real_fun_ops[T].*)(phi[T, S](A!1), u!1(n!1))))))" )"1" "1" expand "*" )"1" expand "phi" )"1" expand "member" )"1" "A!1(x!1)" )"1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "contraction_isf" "mu" "mu!1" "A" "A!1" "f" "u!1(n!1)" ))"1" replace "1" "1" "isf_times_simple_is_isf[T, S, mu!1]" "i" "u!1(n!1)" "h" "phi[T, S](A!1)" ))"1" "(((reals@real_fun_ops[T].*)(phi[T, S](A!1), u!1(n!1))))=(*[T](u!1(n!1), phi[T, S](A!1)))" )"1" "1" "1" expand "*" )"1" expand "phi" )"1" expand "member" )"1" "A!1(x!1)" )"1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" rewrite "phi_is_simple" "2" "A!1" )"2" expand "measurable_set?" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "u!1(n!1)" )"2" expand "isf?" )"2" expand "simple?" )"2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" rewrite "phi_is_simple" "3" "A!1" )"3" expand "measurable_set?" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "w!1" )"2" "u!1" )"2" "2" expand "increasing_nn_isf?" )"2" expand "increasing_nn_simple?" )"2" "2" expand "pointwise_increasing?" )"2" "2" "2" "x!1" )"2" "x!1" )"2" expand "increasing?" )"2" "i!1" "j!1" ))"2" "2" "i!1" "j!1" )"2" "i!1" "j!1" )"2" assert )"2" expand "+" )"2" expand "*" )"2" expand "complement" )"2" expand "phi" )"2" expand "member" )"2" "A!1(x!1)" )"1" assert )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 )"3" expand "nn_isf?" )"3" "3" "1" rewrite "isf_add[T, S, contraction(mu!1, A!1)]" "1" "1" expand "isf?" )"1" "1" rewrite "simple_times" )"1" "w!1" )"1" expand "increasing_nn_simple?" )"1" expand "nn_simple?" )"1" "n!1" )"1" nil nil ))nil ))nil ))nil ))nil )"2" rewrite "phi_is_simple" )"2" "A!1" )"2" "measurable_complement" "a" "A!1" ))"2" expand "measurable_set?" )"2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "nonzero_set?" )"2" expand "*" )"2" expand "complement" )"2" expand "phi" )"2" expand "member" )"2" expand "mu_fin?" )"2" expand "contraction" )"2" expand "intersection" )"2" expand "member" )"2" "{x_1: T | AND IF NOT A!1(x_1) THEN 1 ELSE 0 ENDIF * w!1(n!1)(x_1) /= 0}=emptyset[T]") "1" "mu!1" )"1" expand "measure?" )"1" "1" expand "measure_empty?" )"1" replace "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "emptyset" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "u!1(n!1)" )"2" "contraction_isf" "mu" "mu!1" "A" "A!1" "f" "((reals@real_fun_ops[T].*)(phi[T, S](A!1), u!1(n!1)))" ))"1" replace -1)"1" "1" "(((reals@real_fun_ops[T].*) ") "1" "1" "isf_times_simple_is_isf[T, S, mu!1]" "i" "u!1(n!1)" "h" "phi[T,S](A!1)" ))"1" expand "*" )"1" expand "phi" )"1" expand "member" )"1" "(LAMBDA (x: T): u!1(n!1)(x) * IF A!1(x) THEN 1 ELSE 0 ENDIF)=(LAMBDA (x: T): IF A!1(x) THEN 1 ELSE 0 ENDIF * u!1(n!1)(x))" )"1" "1" "A!1(x!1)" )"1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" rewrite "phi_is_simple" "2" "A!1" )"2" expand "measurable_set?" )"2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "*" )"2" expand "phi" )"2" expand "member" )"2" "A!1(x!1)" )"1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "isf?" )"2" "2" "2" rewrite "simple_times" )"2" rewrite "phi_is_simple" )"2" "A!1" )"2" expand "measurable_set?" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "+" )"2" expand "*" )"2" "2" expand "phi" )"2" expand "complement" )"2" expand "member" )"2" "A!1(x!1)" )"1" "u!1(n!1)" )"1" expand "nn_isf?" )"1" "x!1" )"1" assert )nil nil ))nil ))nil ))nil )"2" assert )"2" "w!1" )"2" expand "increasing_nn_simple?" )"2" "2" expand "nn_simple?" )"2" "n!1" )"2" "2" "x!1" )"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 ))nil ))nil ))nil ))nil )"bool" nn_integral nil )"increasing_nn_isf[T, S, contraction(mu!1, A!1)]" nil )nil nn_integral nil )"bool" nn_integral nil )nil sequences nil )nil nn_integral nil )"bool" nn_integral nil )nil isf nil )"measure_type" measure_contraction nil )"measurable_set[T, S]" measure_contractionnil )nil measure_space_def nil )"bool" measure_space_def nil )"nat" measure_space nil )set type-eq-decl nil sets nil )"[T -> real]" real_fun_ops "reals/" )"bool" isf nil )"measure_type[T, S]" measure_contractionnil )nil generalized_measure_defnil )"bool" generalized_measure_def nil )nil extended_nnreal"extended_nnreal/" )nil real_types nil )"sigma_algebra" measure_contraction nil )nil subset_algebra_def nil )"bool" subset_algebra_def nil )nil sets nil )nil defined_types nil )nil measure_contraction nil )AND const-decl "[bool, bool -> bool]" booleans 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 )"T3" function_props nil )nil measure_space nil )"bool" measure_space nil )nil measure_contraction nil )NOT const-decl "[bool -> bool]" booleans nil )nil measure_contraction nil )"[T, T -> boolean]" equalities nil )"real" isf nil )"bool" topological_convergence "topology/" )"bool" pointwise_convergencenil )"real" reals nil )"(total_order?[real])" nil )"bool" topological_convergence"topology/" )"bool" sets nil )"bool" pointwise_convergence nil )"(total_order?[real])" nil )"bool" real_fun_preds "reals/" )"real" reals nil )nil measure_space nil )"bool" measure_space nil )"bool" pointwise_convergencenil )"measurable_set" nil )"increasing_nn_simple[T, S]" nil )nil measure_space nil )"bool" measure_space nil )nil measure_space_defnil )"bool" measure_space_def nil )"set" sets nil )"increasing_nn_isf[T, S, mu!1]" nil )"[T -> real]" real_fun_ops "reals/" )"boolean" notequal nil )nil measure_space_def nil )nil measure_space nil )"bool" measure_space nil )"bool" metric_space_def"metric_space/" )"odd_int" integers nil )"(strict_total_order?[real])" real_props nil )"real" reals 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 )"set[T]" metric_space_def "metric_space/" )nil real_types nil )"bool" reals nil )"T" measure_contraction nil )"nat" measure_contraction nil )"(strict_total_order?[real])" real_props nil )nil metric_space"metric_space/" )"[numfield, numfield -> numfield]" number_fields nil )nil real_types 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 )"bool" reals nil )"bool" measure_props nil )nil measure_props nil )"set" sets nil )"set[T]" isf nil )"bool" sets nil )"bool" extended_nnreal "extended_nnreal/" )nil isf nil )nil measure_space_def nil )"T" measure_contraction nil )IF const-decl "[boolean, T, T -> T]" if_def nil )nil measure_space nil )nil isf nil )"set" sets nil )"(S)" measure_contractionnil )"measurable_set" nil )"finite_set[T]" sigma_countable"sigma_set/" )"finite_set[T]" countable_setofsets"sets_aux/" )"finite_set[T]" countable_props"sets_aux/" )"finite_set" finite_sets nil )"bool" generalized_measure_def nil )"non_empty_finite_set[real]" measure_space nil )"compact[real, (metric_induced_topology)]" convergence_aux"metric_space/" )"closed[real, (metric_induced_topology)]" convergence_aux"metric_space/" )nil sigma_countable "sigma_set/" )"bool" countability "sets_aux/" )nil countability "sets_aux/" )"set[R]" function_image nil )"set" sets nil )"set[D]" function_image nil )"bool" sets nil )"(singleton?)" sets nil )"[bool, bool -> bool]" booleans nil )"nnreal" measure_props nil )nil isf nil )nil isf nil )"real" reals nil )nil measure_space nil ))nil 3431698665"" (skosimp)"" (split)"1" (grind) nil nil )"2" (typepred "f!1" )"2" (rewrite "contraction_nn_integrable" )"2" (hide 2)"2" (expand "nn_measurable?" )"2" (split)"1" "nn_integrable_is_measurable[T, S, contraction(mu!1, A!1)]" )"1" (inst - "f!1" ) nil nil )) nil )"2" (skosimp)"2" (hide -1) (("2" (grind) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"nnreal" nil )"(total_order?[real])" nil )"bool" sets nil )"nat" measure_space nil )"[T -> real]" real_fun_ops "reals/" )"real" reals nil )nil measure_contractionnil )"bool" measure_space nil )nil measure_space nil )"(total_order?[real])" nil )nil nn_integral nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil measure_contraction nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil real_types nil )nil defined_types nil )nil sets nil )"bool" subset_algebra_def nil )nil subset_algebra_def nil )"sigma_algebra" measure_contraction nil )nil extended_nnreal"extended_nnreal/" )"bool" generalized_measure_def nil )nil generalized_measure_defnil )set type-eq-decl nil sets nil )"bool" measure_space_def nil )nil measure_space_def nil )"measure_type" measure_contraction nil )"bool" nn_integral nil )nil nn_integral nil ))nil ))nil 3431732558"" (skosimp)"" (typepred "f!1" )"" "contraction_nn_integrable" "mu" "mu!1" "A" "A!1" "f" "f!1" ))"1" (assert )"1" (expand "nn_integrable?" )"1" (skosimp*)"1" (expand "nn_integral" )"1" (typepred "u!2" )"1" (typepred "u!1" )"1" "choose_member" "a" "{u: increasing_nn_isf[T, S, contraction(mu!1, A!1)] | ")) "1" case "nonempty?[increasing_nn_isf[T, S, contraction(mu!1, A!1)]] ") "1" "U2" "choose({u: increasing_nn_isf[T, S, contraction(mu!1, A!1)] | ") "1" (split -2)"1" (expand "member" )"1" "1" "nn_convergence[T,S,contraction(mu!1,A!1)]" "u1" "u!2" "u2" "U2" "f" "f!1" ))"1" replace -8)"1" replace -7)"1" replace -2)"1" "1" "U2" )"1" "1" case "nonempty?({u: increasing_nn_isf[T, S, mu!1] | ") "1" "choose_member" "a" "{u: increasing_nn_isf[T, S, mu!1] | ")) "1" "1" "U1" "choose({u: increasing_nn_isf[T, S, mu!1] | ") "1" expand "member" )"1" "1" "nn_convergence[T,S,mu!1]" "u1" "u!1" "u2" "U1" "f" "phi[T, S](A!1)* f!1" ))"1" assert )"1" "1" "U1" )"1" "1" "nn_convergence[T,S,mu!1]" "f" "phi[T, S](A!1)* f!1" "u1" "U1" "u2" "lambda (n:nat): phi[T, S](A!1)*U2(n)" ))"1" assert )"1" "1" "1" replace "1" "1" expand "o" )"1" case "FORALL (n: nat): ") "1" "(LAMBDA (x: nat): isf_integral[T,S,contraction(mu!1,A!1)](U2(x)))=(LAMBDA (x: nat): ") "1" "1" "1" rewrite "contraction_isf_integral" )nil nil ))nil ))nil ))nil )"2" "2" "2" "U2(n!1)" )"2" "contraction_isf" "mu" "mu!1" "A" "A!1" "f" "U2(n!1)" ))"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "pointwise_convergence?" )"2" "2" "x!1" )"2" rewrite "metric_convergence_def" )"2" rewrite "metric_convergence_def" )"2" expand "metric_converges_to" )"2" "2" "r!1" )"2" "2" "n!1" )"2" "2" "i!1" )"2" assert )"2" expand "ball" )"2" expand "*" )"2" expand "phi" )"2" expand "member" )"2" "A!1(x!1)" )"1" assert )nil nil )"2" assert )"2" expand "abs" )"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 )"2" "2" expand "increasing_nn_isf?" )"2" expand "pointwise_increasing?" )"2" "2" "x!1" )"2" expand "increasing?" )"2" "i!1" "j!1" ))"2" "2" "i!1" "j!1" )"2" assert )"2" expand "*" )"2" expand "phi" )"2" expand "member" )"2" "A!1(x!1)" )"1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "3" expand "nn_isf?" )"3" "1" "U2(n!1)" )"1" "contraction_isf" "mu" "mu!1" "A" "A!1" "f" "U2(n!1)" ))"1" assert )nil nil ))nil ))nil )"2" "2" "U2(n!1)" )"2" expand "nn_isf?" )"2" "2" "x!1" )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" "4" "4" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "nonempty?" )"2" nil nil ))nil ))nil ))nil )"2" "2" expand "nonempty?" )"2" expand "empty?" )"2" expand "member" )"2" "u!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "nonempty?" )"2" (propax) nil nil )) nil ))nil ))nil )"2" (hide-all-but (-6 -7 1))"2" (expand "nonempty?" )"2" (expand "empty?" )"2" "u!2" )"2" expand "member" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "nn_measurable?" )"2" (split)"1" "nn_integrable_is_measurable[T,S,contraction(mu!1, A!1)]" )"1" (inst - "f!1" ) nil nil )) nil )"2" (skosimp)"2" (typepred "f!1(x!1)" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil nn_integral nil )"bool" nn_integral nil )"measure_type" measure_contraction nil )nil measure_space_def nil )"bool" measure_space_def nil )set type-eq-decl nil sets nil )nil generalized_measure_defnil )"bool" generalized_measure_def nil )nil extended_nnreal"extended_nnreal/" )"sigma_algebra" measure_contraction nil )nil subset_algebra_def nil )"bool" subset_algebra_def nil )nil sets nil )nil defined_types nil )nil real_types nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil measure_contraction nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil nn_integral nil )nil nn_integral nil )"bool" nn_integral nil )nil sequences nil )nil nn_integral nil )"bool" nn_integral nil )nil isf nil )"bool" isf nil )nil naturalnumbers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil sets_lemmas nil )"bool" pointwise_convergencenil )"(p)" sets nil )"[T, T -> boolean]" equalities nil )"bool" sets nil )nil nn_integral nil )"bool" sets nil )AND const-decl "[bool, bool -> bool]" booleans nil )"T3" function_props nil )nil measure_space nil )"bool" measure_space nil )nil measure_contraction nil )"real" isf nil )"({u: increasing_nn_isf[T, S, contraction(mu!1, A!1)] | " measure_contraction nil) "nn_integrable[T, S, contraction(mu!1, A!1)]" measure_contractionnil )"measurable_set[T, S]" measure_contractionnil )"measure_type[T, S]" measure_contractionnil )nil measure_contraction nil )"metric_open[real, (LAMBDA (x, y: real): abs(x - y))]" "metric_space/" )"(total_order?[real])" nil )"real" reals nil )"nnreal" nil )nil abs_lems "reals/" )"(strict_total_order?[real])" real_props nil )"set[T]" metric_space_def "metric_space/" )"real" reals nil )"bool" reals nil )nil real_types nil )"bool" metric_space_def"metric_space/" )nil metric_space"metric_space/" )nil real_types 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 )"bool" real_fun_preds "reals/" )"(total_order?[real])" nil )"bool" pointwise_convergence nil )"nat" measure_space nil )"[T -> real]" real_fun_ops "reals/" )"bool" sets nil )"nnreal" nn_integral nil )nil measure_contractionnil )"bool" measure_space nil )nil measure_space nil ))nil 3431410319"" (skosimp)"" (rewrite "integrable_pm_def[T, S, contraction(mu!1, A!1)]" )"" (rewrite "integrable_pm_def[T, S, mu!1]" )"" "plus(((reals@real_fun_ops[T].*) ") "1" (hide -1)"1" "minus(((reals@real_fun_ops[T].*) ") "1" (hide -1)"1" "nn_integrable_is_nn_integrable[T,S,contraction(mu!1,A!1)]" )"1" "nn_integrable_is_nn_integrable[T,S,mu!1]" )"1" (split)"1" (flatten)"1" (inst-cp -4 "plus(f!1)" )"1" (inst -4 "minus(f!1)" )"1" (split -4)"1" "1" "1" "contraction_nn_integrable" "mu" "mu!1" "A" "A!1" ))"1" "minus(f!1)" )"1" "plus(f!1)" )"1" assert )"1" "1" rewrite "nn_integrable_is_integrable[T, S, mu!1]" )nil nil )"2" rewrite "nn_integrable_is_integrable[T, S, mu!1]" )nil nil ))nil ))nil )"2" "2" expand "nn_measurable?" )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil )"2" "2" expand "nn_measurable?" )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" (grind) nil nil ))nil ))nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" "((reals@real_fun_ops[T].*) ") "2" (split -4)"1" "((reals@real_fun_ops[T].*) ") "1" "1" "1" "contraction_nn_integrable" "mu" "mu!1" "A" "A!1" ))"1" "minus(f!1)" )"1" "plus(f!1)" )"1" assert )"1" "1" "1" rewrite "nn_integrable_is_integrable[T, S, contraction(mu!1, A!1)]" )nil nil )"2" rewrite "nn_integrable_is_integrable[T, S, contraction(mu!1, A!1)]" )nil nil ))nil ))nil ))nil )"2" expand "nn_measurable?" )"2" "2" (grind) nil nil ))nil ))nil ))nil )"2" expand "nn_measurable?" )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" (grind) nil nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (apply-extensionality :hide? t)"1" (grind) nil nil ) ("2" (grind) nil nil )) nil ))nil ))nil ))nil )"2" (hide 2)"2" (apply-extensionality :hide? t)"1" (grind) nil nil ) ("2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )nil integral nil )"bool" measure_space_def nil )nil measure_space_defnil )nil measure_contraction nil )nil booleans nil )nil booleans nil )nil defined_types nil )nil sets nil )"bool" subset_algebra_def nil )nil subset_algebra_def nil )"sigma_algebra" measure_contraction nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil real_types nil )nil extended_nnreal"extended_nnreal/" )"bool" generalized_measure_def nil )nil generalized_measure_defnil )set type-eq-decl nil sets nil )"bool" measure_space_def nil )nil measure_space_def nil )"measure_type" measure_contraction nil )"measurable_function[T, S]" nil )"measurable_function[T, S]" nil )"[T -> nnreal]" real_fun_ops_aux "reals/" )"[T, T -> boolean]" equalities nil )"[T -> nnreal]" real_fun_ops_aux "reals/" )nil integral nil )"measure_type[T, S]" measure_contractionnil )"measurable_set[T, S]" measure_contractionnil )"bool" integral nil )"measurable_function[T, S]" nil )nil integral nil )"bool" measure_space nil )nil measure_space nil )"(strict_total_order?[real])" real_props nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"real" reals nil )nil nn_integral nil )"bool" nn_integral nil )nil integral nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"(strict_total_order?[real])" real_props nil )nil measure_contractionnil )"real" reals nil )"bool" sets nil )"real" reals nil )"nnreal" nil )"nat" measure_space nil )nil naturalnumbers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"[T -> real]" real_fun_ops "reals/" ))nil 3431409269"" (skosimp)"" (typepred "f!1" )"" (rewrite "contraction_integrable" )"" (hide 2)"" rewrite "integrable_is_measurable[T, S, contraction(mu!1, A!1)]" )nil nil ))nil ))nil ))nil ))nil )nil integral nil )"bool" integral nil )"measure_type" measure_contraction nil )nil measure_space_def nil )"bool" measure_space_def nil )set type-eq-decl nil sets nil )nil generalized_measure_defnil )"bool" generalized_measure_def nil )nil extended_nnreal"extended_nnreal/" )nil real_types nil )"bool" reals nil )"sigma_algebra" measure_contraction nil )nil subset_algebra_def nil )"bool" subset_algebra_def nil )nil sets nil )nil defined_types nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil measure_contraction nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil measure_space_defnil )"bool" measure_space_def nil )nil measure_contraction nil ))nil ))nil 3431766991"" (skosimp)"" (typepred "f!1" )"" "contraction_integrable" "mu" "mu!1" "A" "A!1" "f" "f!1" ))"" (assert )"" (rewrite "integral_pm[T, S, contraction(mu!1, A!1)]" )"" (rewrite "integral_pm[T, S, mu!1]" )"" (rewrite "integrable_pm_def[T, S, mu!1]" )"" (flatten)"" "integrable_pm_def[T, S,contraction(mu!1, A!1)]" "f0" "f!1" ))"" (replace -4 -1)"" (flatten -1)"" (hide -5)"" "contraction_nn_integral" "mu" "mu!1" "A" "A!1" ))"" (rewrite "integral_nn[T, S, mu!1]" )"1" rewrite "integral_nn[T, S, mu!1]" )"1" rewrite "integral_nn[T, S,contraction(mu!1, A!1)]" )"1" rewrite "integral_nn[T, S,contraction(mu!1, A!1)]" )"1" "nn_integrable_is_nn_integrable[T, S, contraction(mu!1, A!1)]" "f" "minus(f!1)" ))"1" "1" "nn_integrable_is_nn_integrable[T, S, contraction(mu!1, A!1)]" "f" "plus(f!1)" ))"1" "1" "1" "minus(f!1)" )"1" "plus(f!1)" )"1" replace -3)"1" replace -4)"1" "1" "plus(((reals@real_fun_ops[T].*) ") "1" "minus(((reals@real_fun_ops[T].*) ") "1" "1" "1" "1" nil nil )"2" nil nil ))nil ))nil ))nil ))nil )"2" "2" "1" nil nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" (grind) nil nil ))nil ))nil ))nil )"2" "2" (grind) nil nil ))nil ))nil ))nil )"2" "2" "nn_integrable_is_nn_integrable[T, S, contraction(mu!1, A!1)]" "f" "minus(f!1)" ))"2" "1" (propax) nil nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "nn_integrable_is_nn_integrable[T, S, contraction(mu!1, A!1)]" "f" "plus(f!1)" ))"2" "1" (propax) nil nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "nn_integrable_is_nn_integrable[T, S, mu!1]" "f" "minus(((reals@real_fun_ops[T].*) ")) "2" "1" (propax) nil nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "nn_integrable_is_nn_integrable[T, S, mu!1]" "f" "plus(((reals@real_fun_ops[T].*) ")) "2" "1" (propax) 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 )nil integral nil )"bool" integral nil )"measure_type" measure_contraction nil )nil measure_space_def nil )"bool" measure_space_def nil )set type-eq-decl nil sets nil )nil generalized_measure_defnil )"bool" generalized_measure_def nil )nil extended_nnreal"extended_nnreal/" )nil real_types nil )"bool" reals nil )"sigma_algebra" measure_contraction nil )nil subset_algebra_def nil )"bool" subset_algebra_def nil )nil sets nil )nil defined_types nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil measure_contraction nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"nat" measure_space nil )nil naturalnumbers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"[T -> real]" real_fun_ops "reals/" )"[T -> nnreal]" real_fun_ops_aux "reals/" )nil nn_integral nil )"bool" nn_integral nil )nil integral nil )"odd_int" integers nil )nil integral nil )"[T, T -> boolean]" equalities nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"bool" sets nil )"[numfield -> numfield]" number_fields nil )"integrable[T, S, contraction(mu!1, A!1)]" nil )"measure_type[T, S]" measure_contractionnil )"bool" reals nil )"measurable_set[T, S]" measure_contractionnil )IF const-decl "[boolean, T, T -> T]" if_def nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"real" reals nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"nnreal" nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"(strict_total_order?[real])" real_props nil )"[T -> nnreal]" real_fun_ops_aux "reals/" )nil measure_contraction nil )nil integral nil )"real" reals nil )"integrable" nil )"measurable_function[T, S]" nil )"integrable" nil )"measurable_function[T, S]" nil )nil integral nil )nil measure_contraction nil )"bool" measure_space_def nil )nil measure_space_defnil ))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ 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.406Bemerkung:
(vorverarbeitet am 2026-04-28)
¤ *Bot Zugriff
2026-05-26
