Quelle monotone_classes.prf
Sprache: Lisp
(monotone_classesnil 3453992461"" (skosimp)"" (skolem + "a!1" )"" (typepred "a!1" )"" (lemma "generated_sigma_algebra_subset1" ("X" "C" ))"" (expand "subset?" )"" (inst - "a!1" ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )nil sets nil )nil defined_types nil )nil nil )"(S)" nil )"(S)" nil )"bool" sets nil )"bool" sets nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil monotone_classes nil )set type-eq-decl nil sets nil )"bool" sets nil )"(nonempty?[set[T]])" monotone_classes nil ))nil ))nil 3454001130"" (skosimp)"" (name "S" "generated_sigma_algebra(C)" )"" (name "TT" "{E:(S) | mu!1(E)=nu!1(E)}" )"1" (case "forall (x:set[T]): S(x) => TT(x)" )"1" (skosimp)"1" (typepred "x!1" )"1" (inst - "x!1" )"1" (expand "S" )"1" (expand "TT" ) (("1" (propax) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skosimp)"2" case "generated_sigma_algebra(generated_subset_algebra(C))=S" )"1" "monotone_class[T]" "B" "generated_subset_algebra[T](C)" "C" "{x:set[T] | S(x) & mu!1(x) = nu!1(x)}" ))"1" (replace -2 -1)"1" (split)"1" (expand "subset?" )"1" (inst - "x!1" )"1" (expand "member" )"1" (assert )"1" expand "TT" )"1" (propax) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -3 2)"2" (expand "subset?" )"2" (skosimp)"2" (expand "member" )"2" "disjoint_algebra_construction" "NX" "C" ))"2" replace -7)"2" expand "member" )"2" "generated_sigma_algebra_subset1[T]" "X" "generated_subset_algebra(C)" ))"2" expand "subset?" -1)"2" "x!2" )"2" expand "member" )"2" assert )"2" replace -2 -3)"2" "2" expand "finite_disjoint_unions" )"2" expand "fullset" )"2" expand "extend" )"2" "2" expand "finite_disjoint_union?" )"2" "2" expand "member" )"2" "mu!1" )"2" "nu!1" )"2" expand "finite_measure?" )"2" "2" case "disjoint_indexed_measurable?[T, (generated_sigma_algebra(C))](E!1)" )"1" "E!1" )"1" "E!1" )"1" replace "1" "1" "zero_tail_series_limit" "n" "n!1" "a" "nu!1 o E!1" ))"1" "1" "zero_tail_series_limit" "n" "n!1" "a" "mu!1 o E!1" ))"1" "1" rewrite "convergence_sequences.limit_def" "1" rewrite "convergence_sequences.limit_def" "1" replace "1" replace "1" replace "1" replace "1" "1" expand "o " )"1" expand "series" )"1" "sigma_eq" "low" "0" "high" "n!1" "F" "LAMBDA (x: nat): mu!1(E!1(x))" "G" "LAMBDA (x: nat): nu!1(E!1(x))" ))"1" assert )"1" "1" "1" "n!2" )"1" "1" assert )"1" "n!2" )"1" expand "<=" "1" "1" assert )"1" "E!1(n!2)" )nil nil ))nil )"2" assert )"2" rewrite "emptyset_is_empty?" )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 "o " )"2" "m!1" )"2" "2" assert )"2" rewrite "emptyset_is_empty?" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "o " )"2" "m!1" )"2" "2" assert )"2" rewrite "emptyset_is_empty?" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "disjoint_indexed_measurable?" )"2" nil nil ))nil ))nil )"3" "3" "n!2" )"3" "n!2" )"3" "3" "n!2<n!1" )"1" "generated_sigma_algebra_subset1[T]" "X" "C" ))"1" expand "subset?" )"1" "E!1(n!2)" )"1" assert )nil nil ))nil ))nil ))nil )"2" assert )"2" rewrite "emptyset_is_empty?" )"2" "generated_sigma_algebra[T](C)" )"2" expand "sigma_algebra?" )"2" "2" expand "subset_algebra_empty?" )"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 ))nil ))nil ))nil ))nil )"2" (hide 2 -3)"2" (expand "monotone?" )"2" (skosimp)"2" (expand "member" )"2" "sigma_algebra_IUnion[T,S]" "SS" "E!1" ))"1" "sigma_algebra_IIntersection[T,S]" "SS" "E!1" ))"1" expand "member" )"1" replace -1)"1" replace -2)"1" "1" "1" "m_increasing_convergence[T,S,to_measure(mu!1)]" "E" "E!1" ))"1" assert )"1" "m_increasing_convergence[T,S,to_measure(nu!1)]" "E" "E!1" ))"1" assert )"1" expand "to_measure" )"1" "MU" "mu!1(IUnion(E!1))" )"1" "NU" "nu!1(IUnion(E!1))" )"1" expand "o " )"1" expand "x_converges?" )"1" "convergence_sequences.convergent?(LAMBDA (i:nat): nu!1(E!1(i)))" )"1" "convergence_sequences.convergent?(LAMBDA (i:nat): mu!1(E!1(i)))" )"1" "convergence_sequences.limit_lemma" "v" "LAMBDA (i: nat): nu!1(E!1(i))" ))"1" "convergence_sequences.limit_lemma" "v" "LAMBDA (i: nat): mu!1(E!1(i))" ))"1" replace "1" replace "1" "cnv_seq_diff" "s1" "LAMBDA (i: nat): mu!1(E!1(i))" "l1" "MU" "s2" "LAMBDA (i: nat): nu!1(E!1(i))" "l2" "NU" ))"1" assert )"1" "cnv_seq_const" "a" "0" ))"1" expand "const_fun" )"1" expand "-" "1" "(LAMBDA (x: nat): mu!1(E!1(x)) - nu!1(E!1(x)))=(LAMBDA (x: nat): 0)" )"1" "convergence_sequences.unique_limit" "u" "LAMBDA (x: nat): 0" "l1" "0" "l2" "MU-NU" ))"1" assert )nil nil ))nil )"2" "1" "x!2" )"1" "1" assert )nil nil ))nil ))nil )"2" "2" "x!2" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil )"2" nil nil )"3" "3" assert )"3" "i!1" )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil )"3" "3" "i!1" )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil )"2" assert )nil nil )"3" "3" "i!1" )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "1" "1" assert )"1" replace -8)"1" assert )nil nil ))nil ))nil ))nil )"2" "2" "to_measure[T, (generated_sigma_algebra(C))](nu!1)" )"2" expand "measure?" )"2" expand "to_measure" )"2" expand "measure_empty?" )"2" "2" assert )"2" expand "measure_countably_additive?" )"2" "2" "X!1" )"2" expand "o " )"2" "X!1" )"2" "2" "1" "1" assert )nil nil ))nil )"2" expand "disjoint_indexed_measurable?" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "n!1" )"2" expand "measurable_set?" )"2" "n!1" )"2" nil nil ))nil ))nil ))nil )"3" "1" "1" replace -7)"1" assert )nil nil ))nil ))nil )"2" "to_measure[T, (generated_sigma_algebra(C))](mu!1)" )"2" "2" expand "measure?" )"2" "2" expand "measure_empty?" )"2" expand "to_measure" )"2" assert )"2" "2" expand "measure_countably_additive?" )"2" "2" "X!1" )"1" expand "o " )"1" nil nil ))nil )"2" "2" "1" "1" assert )nil nil ))nil )"2" "X!1" )"2" expand "disjoint_indexed_measurable?" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "m_decreasing_convergence[T,S,to_measure(mu!1)]" "E" "E!1" ))"1" "m_decreasing_convergence[T,S,to_measure(nu!1)]" "E" "E!1" ))"1" assert )"1" expand "mu_fin?" )"1" expand "to_measure" "1" expand "to_measure" "1" expand "to_measure" "1" expand "o " )"1" expand "x_converges?" )"1" "convergence_sequences.convergent?(LAMBDA (i:nat): nu!1(E!1(i)))" )"1" "convergence_sequences.convergent?(LAMBDA (i:nat): mu!1(E!1(i)))" )"1" "convergence_sequences.limit_def" "v" "LAMBDA (i: nat): mu!1(E!1(i))" "l" "mu!1(IIntersection(E!1))" ))"1" assert )"1" "convergence_sequences.limit_def" "v" "LAMBDA (i: nat): nu!1(E!1(i))" "l" "nu!1(IIntersection(E!1))" ))"1" assert )"1" "cnv_seq_diff" "s1" "LAMBDA (i: nat): nu!1(E!1(i))" "l1" "nu!1(IIntersection(E!1))" "s2" "LAMBDA (i: nat): mu!1(E!1(i))" "l2" "mu!1(IIntersection(E!1))" ))"1" assert )"1" expand "-" "1" "cnv_seq_const" "a" "0" ))"1" expand "const_fun" )"1" "(LAMBDA (x: nat): nu!1(E!1(x)) - mu!1(E!1(x)))=(LAMBDA (x: nat): 0)" )"1" "convergence_sequences.unique_limit" "u" "LAMBDA (x: nat): 0" "l1" "0" "l2" "nu!1(IIntersection(E!1)) - mu!1(IIntersection(E!1))" ))"1" assert )nil nil ))nil )"2" "1" "E!1(x!2)" )"1" assert )nil nil )"2" "x!2" )"2" "2" assert )nil nil ))nil ))nil ))nil )"2" "2" "x!2" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil )"3" "3" "i!1" )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil )"2" assert )nil nil )"3" "3" "i!1" )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil )"2" assert )nil nil )"3" "3" "i!1" )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace -8)"2" "1" "1" assert )nil nil ))nil )"2" "2" "to_measure[T, (generated_sigma_algebra(C))](nu!1)" )"2" expand "measure?" )"2" expand "to_measure" )"2" expand "measure_empty?" )"2" "2" assert )"2" expand "measure_countably_additive?" )"2" "2" "X!1" )"2" expand "o " )"2" "X!1" )"2" "1" "1" assert )"1" "X!1(x1!1)" )"1" expand "S" )"1" nil nil ))nil ))nil ))nil ))nil )"2" expand "disjoint_indexed_measurable?" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "measurable_set?" )"2" "x1!1" )"2" nil nil ))nil ))nil ))nil )"3" replace -7)"3" "1" "1" assert )nil nil ))nil )"2" "2" "to_measure[T, (generated_sigma_algebra(C))](mu!1)" )"2" expand "to_measure" )"2" expand "measure?" )"2" expand "measure_empty?" )"2" "2" assert )"2" expand "measure_countably_additive?" )"2" "2" "X!1" )"2" expand "o " )"2" "X!1" )"2" "1" "1" "X!1(x1!1)" )"1" expand "S" )"1" nil nil ))nil ))nil ))nil )"2" expand "disjoint_indexed_measurable?" )"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 )"2" (skosimp)"2" "x1!1" )"2" (flatten) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (skosimp) (("3" (assert ) nil nil )) nil ))nil )"2" (replace -3 1 rl)"2" (hide-all-but 1)"2" "generated_subset_algebra_subset1" "X" "C" ))"2" "generated_sigma_algebra_subset2" "X" "C" "Y" "generated_sigma_algebra(generated_subset_algebra(C))" ))"2" (assert )"2" (split -1)"1" "generated_sigma_algebra_subset2" "X" "generated_subset_algebra(C)" "Y" "generated_sigma_algebra(C)" ))"1" assert )"1" "1" "1" expand "subset?" )"1" "x!2" )"1" "x!2" )"1" expand "member" )"1" "LHS" "generated_sigma_algebra(generated_subset_algebra(C))(x!2)" )"1" "RHS" "generated_sigma_algebra(C)(x!2)" )"1" "1" assert )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "sigma_algebra_is_subset_algebra[T]" )"2" "generated_sigma_algebra(C)" )"2" "generated_subset_algebra_subset2[T]" "X" "C" "Y" "generated_sigma_algebra[T](C)" ))"2" assert )"2" "2" rewrite "generated_sigma_algebra_subset1[T]" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" expand "subset?" )"2" "2" expand "member" )"2" "x!2" )"2" assert )"2" "generated_sigma_algebra_subset1" "X" "generated_subset_algebra(C)" ))"2" expand "subset?" )"2" "x!2" )"2" expand "member" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp)"2" (typepred "E!1" )"2" (expand "S" ) (("2" (propax) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )"(nonempty?[set[T]])" monotone_classes nil )"bool" sets nil )set type-eq-decl nil sets nil )"sigma_algebra" nil )nil subset_algebra_def nil )"bool" subset_algebra_def nil )"[T, T -> boolean]" equalities nil )nil sets nil )nil defined_types nil )nil booleans nil )nil booleans nil )nil monotone_classes nil )"[bool, bool -> bool]" booleans nil )NOT const-decl "[bool -> bool]" booleans nil )"sigma_algebra[T]" monotone_classes nil )"[(S) -> boolean]" monotone_classes nil )nil nil )"(partial_order?[set[T]])" nil )nil nil )nil nil )nil nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil subset_algebra_def nil )"bool" subset_algebra_def nil )nil subset_algebra_def nil )"(S)" nil )"bool" sets nil )"(S)" nil )"bool" sets nil )nil nil )"set" sets nil )"(S)" sigma_algebranil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )"bool" nil )nil sequences nil )nil sigma "reals/" )OR const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil sigma "reals/" )nil sigma "reals/" )nil integers nil )"(total_order?[real])" nil )nil sets_lemmas nil )"finite_set" finite_sets nil )"finite_set[T]" countable_props"sets_aux/" )"finite_set[T]" countable_setofsets"sets_aux/" )"(S)" monotone_classes nil )"nnreal" sigma_nat "reals/" )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil convergence_sequences "analysis/" )"bool" convergence_sequences "analysis/" )"sequence[real]" series "series/" )"T3" function_props nil )nil series_aux "series/" )nil nil )"sequence[set[T]]" monotone_classes nil )"bool" subset_algebra_def nil )"bool" reals nil )"bool" subset_algebra_def nil )"R" extend nil )"setofsets[T]" nil )nil subset_algebra_defnil )nil sigma_algebra nil )nil measure_props nil )"bool" measure_space_def nil )nil measure_space_def nil )nil extended_nnreal"extended_nnreal/" )"bool" generalized_measure_def nil )nil generalized_measure_defnil )"measure_type" generalized_measure_def nil )"[bool, bool -> bool]" booleans nil )"bool" extended_nnreal "extended_nnreal/" )"[T -> real]" real_fun_ops "reals/" )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"real" reals nil )nil convergence_sequences "analysis/" )"sequence[set[T]]" monotone_classes nil )"[T -> real]" real_fun_ops "reals/" )nil convergence_ops "analysis/" )nil convergence_ops "analysis/" )nil convergence_sequences "analysis/" )"set[T]" indexed_sets nil )"bool" nil )"disjoint_indexed_measurable[T, S]" nil )"bool" generalized_measure_def nil )"disjoint_indexed_measurable[T, S]" nil )nil measure_props nil )"disjoint_indexed_measurable[T, S]" nil )"nat" monotone_classes nil )"set[T]" indexed_sets nil )"bool" measure_props nil )"disjoint_indexed_measurable[T, S]" nil )nil sigma_algebra nil )"subset_algebra" nil )nil subset_algebra_def nil )"bool" subset_algebra_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 )"bool" generalized_measure_def nil )nil generalized_measure_defnil ))nil )nil 3453992723"" (skosimp)"" (name "S" "generated_sigma_algebra(C)" )"" (name "TT" "{E:(S) | mu!1(E)=nu!1(E)}" )"1" (case "forall (x:set[T]): S(x) => TT(x)" )"1" (skosimp)"1" (typepred "x!1" )"1" (inst - "x!1" )"1" (expand "S" )"1" (expand "TT" ) (("1" (propax) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skosimp)"2" case "generated_sigma_algebra(generated_subset_algebra(C))=S" )"1" "monotone_class[T]" "B" "generated_subset_algebra[T](C)" "C" "{x:set[T] | S(x) & mu!1(x) = nu!1(x)}" ))"1" (replace -2 -1)"1" (split)"1" (expand "subset?" )"1" (inst - "x!1" )"1" (expand "member" )"1" (assert )"1" expand "TT" )"1" (propax) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -3 2)"2" (expand "subset?" )"2" (skosimp)"2" (expand "member" )"2" "disjoint_algebra_construction" "NX" "C" ))"2" replace -7)"2" expand "member" )"2" "generated_sigma_algebra_subset1[T]" "X" "generated_subset_algebra(C)" ))"2" expand "subset?" -1)"2" "x!2" )"2" expand "member" )"2" assert )"2" replace -2 -3)"2" "2" expand "finite_disjoint_unions" )"2" expand "fullset" )"2" expand "extend" )"2" "2" expand "finite_disjoint_union?" )"2" "2" expand "member" )"2" "mu!1" )"2" "nu!1" )"2" expand "finite_measure?" )"2" "2" case "disjoint_indexed_measurable?[T, (generated_sigma_algebra(C))](E!1)" )"1" "E!1" )"1" "E!1" )"1" replace "1" "1" "zero_tail_series_limit" "n" "n!1" "a" "nu!1 o E!1" ))"1" "1" "zero_tail_series_limit" "n" "n!1" "a" "mu!1 o E!1" ))"1" "1" rewrite "convergence_sequences.limit_def" "1" rewrite "convergence_sequences.limit_def" "1" replace "1" replace "1" replace "1" replace "1" "1" expand "o " )"1" expand "series" )"1" "sigma_eq" "low" "0" "high" "n!1" "F" "LAMBDA (x: nat): mu!1(E!1(x))" "G" "LAMBDA (x: nat): nu!1(E!1(x))" ))"1" assert )"1" "1" "1" "n!2" )"1" "1" assert )"1" "n!2" )"1" expand "<=" "1" "1" assert )"1" "E!1(n!2)" )nil nil ))nil )"2" assert )"2" rewrite "emptyset_is_empty?" )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 "o " )"2" "m!1" )"2" "2" assert )"2" rewrite "emptyset_is_empty?" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "o " )"2" "m!1" )"2" "2" assert )"2" rewrite "emptyset_is_empty?" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "disjoint_indexed_measurable?" )"2" nil nil ))nil ))nil )"3" "3" "n!2" )"3" "n!2" )"3" "3" "n!2<n!1" )"1" "generated_sigma_algebra_subset1[T]" "X" "C" ))"1" expand "subset?" )"1" "E!1(n!2)" )"1" assert )nil nil ))nil ))nil ))nil )"2" assert )"2" rewrite "emptyset_is_empty?" )"2" "generated_sigma_algebra[T](C)" )"2" expand "sigma_algebra?" )"2" "2" expand "subset_algebra_empty?" )"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 ))nil ))nil ))nil ))nil )"2" (hide 2 -3)"2" (expand "monotone?" )"2" (skosimp)"2" (expand "member" )"2" "sigma_algebra_IUnion[T,S]" "SS" "E!1" ))"1" "sigma_algebra_IIntersection[T,S]" "SS" "E!1" ))"1" expand "member" )"1" replace -1)"1" replace -2)"1" "1" "1" "m_increasing_convergence[T,S,to_measure(mu!1)]" "E" "E!1" ))"1" assert )"1" "m_increasing_convergence[T,S,to_measure(nu!1)]" "E" "E!1" ))"1" assert )"1" expand "to_measure" )"1" "MU" "mu!1(IUnion(E!1))" )"1" "NU" "nu!1(IUnion(E!1))" )"1" expand "o " )"1" expand "x_converges?" )"1" "convergence_sequences.convergent?(LAMBDA (i:nat): nu!1(E!1(i)))" )"1" "convergence_sequences.convergent?(LAMBDA (i:nat): mu!1(E!1(i)))" )"1" "convergence_sequences.limit_lemma" "v" "LAMBDA (i: nat): nu!1(E!1(i))" ))"1" "convergence_sequences.limit_lemma" "v" "LAMBDA (i: nat): mu!1(E!1(i))" ))"1" replace "1" replace "1" "cnv_seq_diff" "s1" "LAMBDA (i: nat): mu!1(E!1(i))" "l1" "MU" "s2" "LAMBDA (i: nat): nu!1(E!1(i))" "l2" "NU" ))"1" assert )"1" "cnv_seq_const" "a" "0" ))"1" expand "const_fun" )"1" expand "-" "1" "(LAMBDA (x: nat): mu!1(E!1(x)) - nu!1(E!1(x)))=(LAMBDA (x: nat): 0)" )"1" "convergence_sequences.unique_limit" "u" "LAMBDA (x: nat): 0" "l1" "0" "l2" "MU-NU" ))"1" assert )nil nil ))nil )"2" "1" "x!2" )"1" "1" assert )nil nil ))nil ))nil )"2" "2" "x!2" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil )"2" nil nil )"3" "3" assert )"3" "i!1" )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil )"3" "3" "i!1" )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil )"2" assert )nil nil )"3" "3" "i!1" )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "1" "1" assert )"1" replace -8)"1" assert )nil nil ))nil ))nil ))nil )"2" "2" "to_measure[T, (generated_sigma_algebra(C))](nu!1)" )"2" expand "measure?" )"2" expand "to_measure" )"2" expand "measure_empty?" )"2" "2" assert )"2" expand "measure_countably_additive?" )"2" "2" "X!1" )"2" expand "o " )"2" "X!1" )"2" "2" "1" "1" assert )nil nil ))nil )"2" expand "disjoint_indexed_measurable?" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "n!1" )"2" expand "measurable_set?" )"2" "n!1" )"2" nil nil ))nil ))nil ))nil )"3" "1" "1" replace -7)"1" assert )nil nil ))nil ))nil )"2" "to_measure[T, (generated_sigma_algebra(C))](mu!1)" )"2" "2" expand "measure?" )"2" "2" expand "measure_empty?" )"2" expand "to_measure" )"2" assert )"2" "2" expand "measure_countably_additive?" )"2" "2" "X!1" )"1" expand "o " )"1" nil nil ))nil )"2" "2" "1" "1" assert )nil nil ))nil )"2" "X!1" )"2" expand "disjoint_indexed_measurable?" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "m_decreasing_convergence[T,S,to_measure(mu!1)]" "E" "E!1" ))"1" "m_decreasing_convergence[T,S,to_measure(nu!1)]" "E" "E!1" ))"1" assert )"1" expand "mu_fin?" )"1" expand "to_measure" "1" expand "to_measure" "1" expand "to_measure" "1" expand "o " )"1" expand "x_converges?" )"1" "convergence_sequences.convergent?(LAMBDA (i:nat): nu!1(E!1(i)))" )"1" "convergence_sequences.convergent?(LAMBDA (i:nat): mu!1(E!1(i)))" )"1" "convergence_sequences.limit_def" "v" "LAMBDA (i: nat): mu!1(E!1(i))" "l" "mu!1(IIntersection(E!1))" ))"1" assert )"1" "convergence_sequences.limit_def" "v" "LAMBDA (i: nat): nu!1(E!1(i))" "l" "nu!1(IIntersection(E!1))" ))"1" assert )"1" "cnv_seq_diff" "s1" "LAMBDA (i: nat): nu!1(E!1(i))" "l1" "nu!1(IIntersection(E!1))" "s2" "LAMBDA (i: nat): mu!1(E!1(i))" "l2" "mu!1(IIntersection(E!1))" ))"1" assert )"1" expand "-" "1" "cnv_seq_const" "a" "0" ))"1" expand "const_fun" )"1" "(LAMBDA (x: nat): nu!1(E!1(x)) - mu!1(E!1(x)))=(LAMBDA (x: nat): 0)" )"1" "convergence_sequences.unique_limit" "u" "LAMBDA (x: nat): 0" "l1" "0" "l2" "nu!1(IIntersection(E!1)) - mu!1(IIntersection(E!1))" ))"1" assert )nil nil ))nil )"2" "1" "E!1(x!2)" )"1" assert )nil nil )"2" "x!2" )"2" "2" assert )nil nil ))nil ))nil ))nil )"2" "2" "x!2" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil )"3" "3" "i!1" )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil )"2" assert )nil nil )"3" "3" "i!1" )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil )"2" assert )nil nil )"3" "3" "i!1" )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace -8)"2" "1" "1" assert )nil nil ))nil )"2" "2" "to_measure[T, (generated_sigma_algebra(C))](nu!1)" )"2" expand "measure?" )"2" expand "to_measure" )"2" expand "measure_empty?" )"2" "2" assert )"2" expand "measure_countably_additive?" )"2" "2" "X!1" )"2" expand "o " )"2" "X!1" )"2" "1" "1" assert )"1" "X!1(x1!1)" )"1" expand "S" )"1" nil nil ))nil ))nil ))nil ))nil )"2" expand "disjoint_indexed_measurable?" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "measurable_set?" )"2" "x1!1" )"2" nil nil ))nil ))nil ))nil )"3" replace -7)"3" "1" "1" assert )nil nil ))nil )"2" "2" "to_measure[T, (generated_sigma_algebra(C))](mu!1)" )"2" expand "to_measure" )"2" expand "measure?" )"2" expand "measure_empty?" )"2" "2" assert )"2" expand "measure_countably_additive?" )"2" "2" "X!1" )"2" expand "o " )"2" "X!1" )"2" "1" "1" "X!1(x1!1)" )"1" expand "S" )"1" nil nil ))nil ))nil ))nil )"2" expand "disjoint_indexed_measurable?" )"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 )"2" (skosimp)"2" "x1!1" )"2" (flatten) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (skosimp) (("3" (assert ) nil nil )) nil ))nil )"2" (replace -3 1 rl)"2" (hide-all-but 1)"2" "generated_subset_algebra_subset1" "X" "C" ))"2" "generated_sigma_algebra_subset2" "X" "C" "Y" "generated_sigma_algebra(generated_subset_algebra(C))" ))"2" (assert )"2" (split -1)"1" "generated_sigma_algebra_subset2" "X" "generated_subset_algebra(C)" "Y" "generated_sigma_algebra(C)" ))"1" assert )"1" "1" "1" expand "subset?" )"1" "x!2" )"1" "x!2" )"1" expand "member" )"1" "LHS" "generated_sigma_algebra(generated_subset_algebra(C))(x!2)" )"1" "RHS" "generated_sigma_algebra(C)(x!2)" )"1" "1" assert )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "sigma_algebra_is_subset_algebra[T]" )"2" "generated_sigma_algebra(C)" )"2" "generated_subset_algebra_subset2[T]" "X" "C" "Y" "generated_sigma_algebra[T](C)" ))"2" assert )"2" "2" rewrite "generated_sigma_algebra_subset1[T]" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" expand "subset?" )"2" "2" expand "member" )"2" "x!2" )"2" assert )"2" "generated_sigma_algebra_subset1" "X" "generated_subset_algebra(C)" ))"2" expand "subset?" )"2" "x!2" )"2" expand "member" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp)"2" (typepred "E!1" )"2" (expand "S" ) (("2" (propax) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )"bool" measure_props nil )nil measure_props nil )nil convergence_sequences "analysis/" )nil convergence_ops "analysis/" )nil convergence_ops "analysis/" )nil convergence_sequences "analysis/" )"[T -> real]" real_fun_ops "reals/" )"bool" extended_nnreal "extended_nnreal/" )nil extended_nnreal"extended_nnreal/" )nil measure_space_def nil )"bool" measure_space_def nil )nil measure_props nil )nil convergence_sequences "analysis/" )"finite_set" finite_sets nil )nil sigma "reals/" )nil sigma "reals/" )nil sigma "reals/" )nil sequences nil )"set" sets nil )"bool" sets nil )"bool" sets nil )nil sets nil )set type-eq-decl nil sets nil )"bool" sets nil ))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Dauer der Verarbeitung: 0.160 Sekunden
(vorverarbeitet am 2026-04-26)
¤ *© Formatika GbR, Deutschland
2026-05-26
