| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/measure_integration/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 215 kB |
|
Quelle monotone_classes.prfSprache: Lisp |
|||||||||||||||
|
(monotone_classes (monotone_finite_measures_TCC1 0 (monotone_finite_measures_TCC1-1 nil 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) ((setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (generated_sigma_algebra_subset1 formula-decl nil subset_algebra_def nil) (subset_algebra_complement application-judgement "(S)" sigma_algebra nil) (subset_algebra_intersection application-judgement "(S)" sigma_algebra nil) (member const-decl "bool" sets nil) (subset? const-decl "bool" sets nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (T formal-type-decl nil monotone_classes nil) (set type-eq-decl nil sets nil) (nonempty? const-decl "bool" sets nil) (C formal-const-decl "(nonempty?[set[T]])" monotone_classes nil)) nil)) (monotone_finite_measures 0 (monotone_finite_measures-2 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" (lemma "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" (lemma "disjoint_algebra_construction" ("NX" "C")) (("2" (replace -7) (("2" (expand "member") (("2" (lemma "generated_sigma_algebra_subset1[T]" ("X" "generated_subset_algebra(C)")) (("2" (expand "subset?" -1) (("2" (inst - "x!2") (("2" (expand "member") (("2" (assert) (("2" (replace -2 -3) (("2" (hide-all-but (-3 -9 1)) (("2" (expand "finite_disjoint_unions") (("2" (expand "fullset") (("2" (expand "extend") (("2" (prop) (("2" (expand "finite_disjoint_union?") (("2" (skosimp) (("2" (expand "member") (("2" (typepred "mu!1") (("2" (typepred "nu!1") (("2" (expand "finite_measure?") (("2" (flatten) (("2" (case "disjoint_indexed_measurable?[T, (generated_sigma_algebra(C))](E!1)") (("1" (inst - "E!1") (("1" (inst - "E!1") (("1" (replace -7 * rl) (("1" (hide -1 -6 -7) (("1" (lemma "zero_tail_series_limit" ("n" "n!1" "a" "nu!1 o E!1")) (("1" (split) (("1" (lemma "zero_tail_series_limit" ("n" "n!1" "a" "mu!1 o E!1")) (("1" (split) (("1" (rewrite "convergence_sequences.limit_def" -4 :dir rl) (("1" (rewrite "convergence_sequences.limit_def" -6 :dir rl) (("1" (replace -1) (("1" (replace -2) (("1" (replace -4 * rl) (("1" (replace -6 * rl) (("1" (hide -1 -2 -4 -6) (("1" (expand "o ") (("1" (expand "series") (("1" (lemma "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" (hide 2) (("1" (skosimp) (("1" (inst -3 "n!2") (("1" (flatten) (("1" (assert) (("1" (typepred "n!2") (("1" (expand "<=" -2) (("1" (split) (("1" (assert) (("1" (inst -7 "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" (skosimp) (("2" (expand "o ") (("2" (inst -7 "m!1") (("2" (flatten) (("2" (assert) (("2" (rewrite "emptyset_is_empty?") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (expand "o ") (("2" (inst -6 "m!1") (("2" (flatten) (("2" (assert) (("2" (rewrite "emptyset_is_empty?") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 -2 -3 -4 2) (("2" (expand "disjoint_indexed_measurable?") (("2" (propax) nil nil)) nil)) nil) ("3" (hide -1 -2 -3 -4 -6 2 -8) (("3" (skolem + "n!2") (("3" (inst - "n!2") (("3" (flatten) (("3" (case-replace "n!2<n!1") (("1" (lemma "generated_sigma_algebra_subset1[T]" ("X" "C")) (("1" (expand "subset?") (("1" (inst - "E!1(n!2)") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (rewrite "emptyset_is_empty?") (("2" (typepred "generated_sigma_algebra[T](C)") (("2" (expand "sigma_algebra?") (("2" (flatten) (("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" (lemma "sigma_algebra_IUnion[T,S]" ("SS" "E!1")) (("1" (lemma "sigma_algebra_IIntersection[T,S]" ("SS" "E!1")) (("1" (expand "member") (("1" (replace -1) (("1" (replace -2) (("1" (split) (("1" (flatten) (("1" (lemma "m_increasing_convergence[T,S,to_measure(mu!1)]" ("E" "E!1")) (("1" (assert) (("1" (lemma "m_increasing_convergence[T,S,to_measure(nu!1)]" ("E" "E!1")) (("1" (assert) (("1" (expand "to_measure") (("1" (name-replace "MU" "mu!1(IUnion(E!1))") (("1" (name-replace "NU" "nu!1(IUnion(E!1))") (("1" (expand "o ") (("1" (expand "x_converges?") (("1" (case-replace "convergence_sequences.convergent?(LAMBDA (i:nat): nu!1(E!1(i)))") (("1" (case-replace "convergence_sequences.convergent?(LAMBDA (i:nat): mu!1(E!1(i)))") (("1" (lemma "convergence_sequences.limit_lemma" ("v" "LAMBDA (i: nat): nu!1(E!1(i))")) (("1" (lemma "convergence_sequences.limit_lemma" ("v" "LAMBDA (i: nat): mu!1(E!1(i))")) (("1" (replace -5 * rl) (("1" (replace -6 * rl) (("1" (lemma "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" (lemma "cnv_seq_const" ("a" "0")) (("1" (expand "const_fun") (("1" (expand "-" -2) (("1" (case-replace "(LAMBDA (x: nat): mu!1(E!1(x)) - nu!1(E!1(x)))=(LAMBDA (x: nat): 0)") (("1" (lemma "convergence_sequences.unique_limit" ("u" "LAMBDA (x: nat): 0" "l1" "0" "l2" "MU-NU")) (("1" (assert) nil nil)) nil) ("2" (apply-extensionality :hide? t) (("1" (inst -12 "x!2") (("1" (flatten) (("1" (assert) nil nil)) nil)) nil) ("2" (skosimp) (("2" (inst -12 "x!2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil) ("2" (propax) nil nil) ("3" (skosimp) (("3" (assert) (("3" (inst -8 "i!1") (("3" (flatten) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil) ("3" (skosimp) (("3" (inst -7 "i!1") (("3" (flatten) (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil) ("3" (skosimp) (("3" (inst -6 "i!1") (("3" (flatten) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (split) (("1" (skosimp) (("1" (assert) (("1" (replace -8) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide-all-but (1 -9)) (("2" (typepred "to_measure[T, (generated_sigma_algebra(C))](nu!1)") (("2" (expand "measure?") (("2" (expand "to_measure") (("2" (expand "measure_empty?") (("2" (flatten) (("2" (assert) (("2" (expand "measure_countably_additive?") (("2" (skosimp) (("2" (typepred "X!1") (("2" (expand "o ") (("2" (inst - "X!1") (("2" (hide 2) (("2" (split) (("1" (skosimp) (("1" (assert) nil nil)) nil) ("2" (expand "disjoint_indexed_measurable?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skolem + "n!1") (("2" (expand "measurable_set?") (("2" (inst - "n!1") (("2" (flatten) nil nil)) nil)) nil)) nil) ("3" (split) (("1" (skosimp) (("1" (replace -7) (("1" (assert) nil nil)) nil)) nil) ("2" (typepred "to_measure[T, (generated_sigma_algebra(C))](mu!1)") (("2" (hide-all-but (-1 1 -8)) (("2" (expand "measure?") (("2" (flatten) (("2" (expand "measure_empty?") (("2" (expand "to_measure") (("2" (assert) (("2" (hide -1) (("2" (expand "measure_countably_additive?") (("2" (skosimp) (("2" (inst - "X!1") (("1" (expand "o ") (("1" (propax) nil nil)) nil) ("2" (hide 2) (("2" (split) (("1" (skosimp) (("1" (assert) nil nil)) nil) ("2" (typepred "X!1") (("2" (expand "disjoint_indexed_measurable?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (lemma "m_decreasing_convergence[T,S,to_measure(mu!1)]" ("E" "E!1")) (("1" (lemma "m_decreasing_convergence[T,S,to_measure(nu!1)]" ("E" "E!1")) (("1" (assert) (("1" (expand "mu_fin?") (("1" (expand "to_measure" -1 1) (("1" (expand "to_measure" -2 1) (("1" (expand "to_measure" (-1 -2)) (("1" (expand "o ") (("1" (expand "x_converges?") (("1" (case-replace "convergence_sequences.convergent?(LAMBDA (i:nat): nu!1(E!1(i)))") (("1" (case-replace "convergence_sequences.convergent?(LAMBDA (i:nat): mu!1(E!1(i)))") (("1" (lemma "convergence_sequences.limit_def" ("v" "LAMBDA (i: nat): mu!1(E!1(i))" "l" "mu!1(IIntersection(E!1))")) (("1" (assert) (("1" (lemma "convergence_sequences.limit_def" ("v" "LAMBDA (i: nat): nu!1(E!1(i))" "l" "nu!1(IIntersection(E!1))")) (("1" (assert) (("1" (lemma "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) (("1" (lemma "cnv_seq_const" ("a" "0")) (("1" (expand "const_fun") (("1" (case-replace "(LAMBDA (x: nat): nu!1(E!1(x)) - mu!1(E!1(x)))=(LAMBDA (x: nat): 0)") (("1" (lemma "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" (apply-extensionality :hide? t) (("1" (inst -18 "E!1(x!2)") (("1" (assert) nil nil) ("2" (inst - "x!2") (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (inst - "x!2") (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil) ("3" (skosimp) (("3" (inst - "i!1") (("3" (flatten) (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil) ("3" (skosimp) (("3" (inst - "i!1") (("3" (flatten) (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil) ("3" (skosimp) (("3" (inst - "i!1") (("3" (flatten) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -8) (("2" (split) (("1" (skosimp) (("1" (assert) nil nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "to_measure[T, (generated_sigma_algebra(C))](nu!1)") (("2" (expand "measure?") (("2" (expand "to_measure") (("2" (expand "measure_empty?") (("2" (flatten) (("2" (assert) (("2" (expand "measure_countably_additive?") (("2" (skosimp) (("2" (typepred "X!1") (("2" (expand "o ") (("2" (inst - "X!1") (("2" (split) (("1" (skosimp) (("1" (assert) (("1" (typepred "X!1(x1!1)") (("1" (expand "S") (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "disjoint_indexed_measurable?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (expand "measurable_set?") (("2" (inst - "x1!1") (("2" (flatten) nil nil)) nil)) nil)) nil) ("3" (replace -7) (("3" (split) (("1" (skosimp) (("1" (assert) nil nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "to_measure[T, (generated_sigma_algebra(C))](mu!1)") (("2" (expand "to_measure") (("2" (expand "measure?") (("2" (expand "measure_empty?") (("2" (flatten) (("2" (assert) (("2" (expand "measure_countably_additive?") (("2" (skosimp) (("2" (typepred "X!1") (("2" (expand "o ") (("2" (inst - "X!1") (("2" (split) (("1" (skosimp) (("1" (typepred "X!1(x1!1)") (("1" (expand "S") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (expand "disjoint_indexed_measurable?") (("2" (propax) 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" (inst - "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" (lemma "generated_subset_algebra_subset1" ("X" "C")) (("2" (lemma "generated_sigma_algebra_subset2" ("X" "C" "Y" "generated_sigma_algebra(generated_subset_algebra(C))")) (("2" (assert) (("2" (split -1) (("1" (lemma "generated_sigma_algebra_subset2" ("X" "generated_subset_algebra(C)" "Y" "generated_sigma_algebra(C)")) (("1" (assert) (("1" (split -1) (("1" (apply-extensionality :hide? t) (("1" (expand "subset?") (("1" (inst - "x!2") (("1" (inst - "x!2") (("1" (expand "member") (("1" (name-replace "LHS" "generated_sigma_algebra(generated_subset_algebra(C))(x!2)") (("1" (name-replace "RHS" "generated_sigma_algebra(C)(x!2)") (("1" (hide -3) (("1" (assert) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (hide-all-but 1) (("2" (lemma "sigma_algebra_is_subset_algebra[T]") (("2" (inst - "generated_sigma_algebra(C)") (("2" (lemma "generated_subset_algebra_subset2[T]" ("X" "C" "Y" "generated_sigma_algebra[T](C)")) (("2" (assert) (("2" (hide -1 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" (skosimp) (("2" (expand "member") (("2" (inst - "x!2") (("2" (assert) (("2" (lemma "generated_sigma_algebra_subset1" ("X" "generated_subset_algebra(C)")) (("2" (expand "subset?") (("2" (inst - "x!2") (("2" (expand "member") (("2" (propax) 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) ((C formal-const-decl "(nonempty?[set[T]])" monotone_classes nil) (nonempty? const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (generated_sigma_algebra const-decl "sigma_algebra" subset_algebra_def nil) (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil) (sigma_algebra? const-decl "bool" subset_algebra_def nil) (= const-decl "[T, T -> boolean]" equalities nil) (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T formal-type-decl nil monotone_classes nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (S skolem-const-decl "sigma_algebra[T]" monotone_classes nil) (TT skolem-const-decl "[(S) -> boolean]" monotone_classes nil) (generated_subset_algebra_subset1 formula-decl nil subset_algebra_def nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (generated_subset_algebra_subset2 formula-decl nil subset_algebra_def nil) (sigma_algebra_is_subset_algebra judgement-tcc nil subset_algebra_def nil) (generated_sigma_algebra_subset2 formula-decl nil subset_algebra_def nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (monotone_class nonempty-type-eq-decl nil subset_algebra_def nil) (monotone? const-decl "bool" subset_algebra_def nil) (monotone_class formula-decl nil subset_algebra_def nil) (subset_algebra_complement application-judgement "(S)" sigma_algebra nil) (member const-decl "bool" sets nil) (subset_algebra_intersection application-judgement "(S)" sigma_algebra nil) (subset? const-decl "bool" sets nil) (generated_sigma_algebra_subset1 formula-decl nil subset_algebra_def nil) (fullset const-decl "set" sets nil) (sigma_algebra_IUnion_rew application-judgement "(S)" sigma_algebra nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (disjoint_indexed_measurable? const-decl "bool" generalized_measure_def nil) (sequence type-eq-decl nil sequences nil) (sigma_eq formula-decl nil sigma "reals/") (OR const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/") (subrange type-eq-decl nil integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (emptyset_is_empty? formula-decl nil sets_lemmas nil) (finite_emptyset name-judgement "finite_set" finite_sets nil) (finite_emptyset name-judgement "finite_set[T]" countable_props "sets_aux/") (finite_emptyset name-judgement "finite_set[T]" countable_setofsets "sets_aux/") (subset_algebra_emptyset name-judgement "(S)" monotone_classes nil) (sigma_nnreal application-judgement "nnreal" sigma_nat "reals/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (limit_def formula-decl nil convergence_sequences "analysis/") (convergent? const-decl "bool" convergence_sequences "analysis/") (series const-decl "sequence[real]" series "series/") (O const-decl "T3" function_props nil) (zero_tail_series_limit formula-decl nil series_aux "series/") (disjoint_indexed_measurable nonempty-type-eq-decl nil generalized_measure_def nil) (E!1 skolem-const-decl "sequence[set[T]]" monotone_classes nil) (subset_algebra_empty? const-decl "bool" subset_algebra_def nil) (< const-decl "bool" reals nil) (finite_disjoint_union? const-decl "bool" subset_algebra_def nil) (extend const-decl "R" extend nil) (finite_disjoint_unions const-decl "setofsets[T]" subset_algebra_def nil) (disjoint_algebra_construction formula-decl nil subset_algebra_def nil) (sigma_algebra_IIntersection formula-decl nil sigma_algebra nil) (m_increasing_convergence formula-decl nil measure_props nil) (measurable_set? const-decl "bool" measure_space_def nil) (measurable_set nonempty-type-eq-decl nil measure_space_def nil) (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (measure? const-decl "bool" generalized_measure_def nil) (measure_type nonempty-type-eq-decl nil generalized_measure_def nil) (to_measure const-decl "measure_type" generalized_measure_def nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (x_converges? const-decl "bool" extended_nnreal "extended_nnreal/") (const_fun const-decl "[T -> real]" real_fun_ops "reals/") (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (real_minus_real_is_real application-judgement "real" reals nil) (unique_limit formula-decl nil convergence_sequences "analysis/") (E!1 skolem-const-decl "sequence[set[T]]" monotone_classes nil) (- const-decl "[T -> real]" real_fun_ops "reals/") (cnv_seq_const formula-decl nil convergence_ops "analysis/") (cnv_seq_diff formula-decl nil convergence_ops "analysis/") (limit_lemma formula-decl nil convergence_sequences "analysis/") (IUnion const-decl "set[T]" indexed_sets nil) (measure_countably_additive? const-decl "bool" generalized_measure_def nil) (X!1 skolem-const-decl "disjoint_indexed_measurable[T, S]" monotone_classes nil) (measure_empty? const-decl "bool" generalized_measure_def nil) (X!1 skolem-const-decl "disjoint_indexed_measurable[T, S]" monotone_classes nil) (m_decreasing_convergence formula-decl nil measure_props nil) (X!1 skolem-const-decl "disjoint_indexed_measurable[T, S]" monotone_classes nil) (x!2 skolem-const-decl "nat" monotone_classes nil) (IIntersection const-decl "set[T]" indexed_sets nil) (mu_fin? const-decl "bool" measure_props nil) (X!1 skolem-const-decl "disjoint_indexed_measurable[T, S]" monotone_classes nil) (sigma_algebra_IUnion formula-decl nil sigma_algebra nil) (generated_subset_algebra const-decl "subset_algebra" subset_algebra_def nil) (subset_algebra nonempty-type-eq-decl nil subset_algebra_def nil) (subset_algebra? const-decl "bool" subset_algebra_def nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (finite_measure? const-decl "bool" generalized_measure_def nil) (finite_measure nonempty-type-eq-decl nil generalized_measure_def nil)) nil) (monotone_finite_measures-1 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" (lemma "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" (lemma "disjoint_algebra_construction" ("NX" "C")) (("2" (replace -7) (("2" (expand "member") (("2" (lemma "generated_sigma_algebra_subset1[T]" ("X" "generated_subset_algebra(C)")) (("2" (expand "subset?" -1) (("2" (inst - "x!2") (("2" (expand "member") (("2" (assert) (("2" (replace -2 -3) (("2" (hide-all-but (-3 -9 1)) (("2" (expand "finite_disjoint_unions") (("2" (expand "fullset") (("2" (expand "extend") (("2" (prop) (("2" (expand "finite_disjoint_union?") (("2" (skosimp) (("2" (expand "member") (("2" (typepred "mu!1") (("2" (typepred "nu!1") (("2" (expand "finite_measure?") (("2" (flatten) (("2" (case "disjoint_indexed_measurable?[T, (generated_sigma_algebra(C))](E!1)") (("1" (inst - "E!1") (("1" (inst - "E!1") (("1" (replace -7 * rl) (("1" (hide -1 -6 -7) (("1" (lemma "zero_tail_series_limit" ("n" "n!1" "a" "nu!1 o E!1")) (("1" (split) (("1" (lemma "zero_tail_series_limit" ("n" "n!1" "a" "mu!1 o E!1")) (("1" (split) (("1" (rewrite "convergence_sequences.limit_def" -4 :dir rl) (("1" (rewrite "convergence_sequences.limit_def" -6 :dir rl) (("1" (replace -1) (("1" (replace -2) (("1" (replace -4 * rl) (("1" (replace -6 * rl) (("1" (hide -1 -2 -4 -6) (("1" (expand "o ") (("1" (expand "series") (("1" (lemma "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" (hide 2) (("1" (skosimp) (("1" (inst -3 "n!2") (("1" (flatten) (("1" (assert) (("1" (typepred "n!2") (("1" (expand "<=" -2) (("1" (split) (("1" (assert) (("1" (inst -7 "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" (skosimp) (("2" (expand "o ") (("2" (inst -7 "m!1") (("2" (flatten) (("2" (assert) (("2" (rewrite "emptyset_is_empty?") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (expand "o ") (("2" (inst -6 "m!1") (("2" (flatten) (("2" (assert) (("2" (rewrite "emptyset_is_empty?") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 -2 -3 -4 2) (("2" (expand "disjoint_indexed_measurable?") (("2" (propax) nil nil)) nil)) nil) ("3" (hide -1 -2 -3 -4 -6 2 -8) (("3" (skolem + "n!2") (("3" (inst - "n!2") (("3" (flatten) (("3" (case-replace "n!2<n!1") (("1" (lemma "generated_sigma_algebra_subset1[T]" ("X" "C")) (("1" (expand "subset?") (("1" (inst - "E!1(n!2)") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (rewrite "emptyset_is_empty?") (("2" (typepred "generated_sigma_algebra[T](C)") (("2" (expand "sigma_algebra?") (("2" (flatten) (("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" (lemma "sigma_algebra_IUnion[T,S]" ("SS" "E!1")) (("1" (lemma "sigma_algebra_IIntersection[T,S]" ("SS" "E!1")) (("1" (expand "member") (("1" (replace -1) (("1" (replace -2) (("1" (split) (("1" (flatten) (("1" (lemma "m_increasing_convergence[T,S,to_measure(mu!1)]" ("E" "E!1")) (("1" (assert) (("1" (lemma "m_increasing_convergence[T,S,to_measure(nu!1)]" ("E" "E!1")) (("1" (assert) (("1" (expand "to_measure") (("1" (name-replace "MU" "mu!1(IUnion(E!1))") (("1" (name-replace "NU" "nu!1(IUnion(E!1))") (("1" (expand "o ") (("1" (expand "x_converges?") (("1" (case-replace "convergence_sequences.convergent?(LAMBDA (i:nat): nu!1(E!1(i)))") (("1" (case-replace "convergence_sequences.convergent?(LAMBDA (i:nat): mu!1(E!1(i)))") (("1" (lemma "convergence_sequences.limit_lemma" ("v" "LAMBDA (i: nat): nu!1(E!1(i))")) (("1" (lemma "convergence_sequences.limit_lemma" ("v" "LAMBDA (i: nat): mu!1(E!1(i))")) (("1" (replace -5 * rl) (("1" (replace -6 * rl) (("1" (lemma "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" (lemma "cnv_seq_const" ("a" "0")) (("1" (expand "const_fun") (("1" (expand "-" -2) (("1" (case-replace "(LAMBDA (x: nat): mu!1(E!1(x)) - nu!1(E!1(x)))=(LAMBDA (x: nat): 0)") (("1" (lemma "convergence_sequences.unique_limit" ("u" "LAMBDA (x: nat): 0" "l1" "0" "l2" "MU-NU")) (("1" (assert) nil nil)) nil) ("2" (apply-extensionality :hide? t) (("1" (inst -12 "x!2") (("1" (flatten) (("1" (assert) nil nil)) nil)) nil) ("2" (skosimp) (("2" (inst -12 "x!2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil) ("2" (propax) nil nil) ("3" (skosimp) (("3" (assert) (("3" (inst -8 "i!1") (("3" (flatten) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil) ("3" (skosimp) (("3" (inst -7 "i!1") (("3" (flatten) (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil) ("3" (skosimp) (("3" (inst -6 "i!1") (("3" (flatten) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (split) (("1" (skosimp) (("1" (assert) (("1" (replace -8) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide-all-but (1 -9)) (("2" (typepred "to_measure[T, (generated_sigma_algebra(C))](nu!1)") (("2" (expand "measure?") (("2" (expand "to_measure") (("2" (expand "measure_empty?") (("2" (flatten) (("2" (assert) (("2" (expand "measure_countably_additive?") (("2" (skosimp) (("2" (typepred "X!1") (("2" (expand "o ") (("2" (inst - "X!1") (("2" (hide 2) (("2" (split) (("1" (skosimp) (("1" (assert) nil nil)) nil) ("2" (expand "disjoint_indexed_measurable?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skolem + "n!1") (("2" (expand "measurable_set?") (("2" (inst - "n!1") (("2" (flatten) nil nil)) nil)) nil)) nil) ("3" (split) (("1" (skosimp) (("1" (replace -7) (("1" (assert) nil nil)) nil)) nil) ("2" (typepred "to_measure[T, (generated_sigma_algebra(C))](mu!1)") (("2" (hide-all-but (-1 1 -8)) (("2" (expand "measure?") (("2" (flatten) (("2" (expand "measure_empty?") (("2" (expand "to_measure") (("2" (assert) (("2" (hide -1) (("2" (expand "measure_countably_additive?") (("2" (skosimp) (("2" (inst - "X!1") (("1" (expand "o ") (("1" (propax) nil nil)) nil) ("2" (hide 2) (("2" (split) (("1" (skosimp) (("1" (assert) nil nil)) nil) ("2" (typepred "X!1") (("2" (expand "disjoint_indexed_measurable?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (lemma "m_decreasing_convergence[T,S,to_measure(mu!1)]" ("E" "E!1")) (("1" (lemma "m_decreasing_convergence[T,S,to_measure(nu!1)]" ("E" "E!1")) (("1" (assert) (("1" (expand "mu_fin?") (("1" (expand "to_measure" -1 1) (("1" (expand "to_measure" -2 1) (("1" (expand "to_measure" (-1 -2)) (("1" (expand "o ") (("1" (expand "x_converges?") (("1" (case-replace "convergence_sequences.convergent?(LAMBDA (i:nat): nu!1(E!1(i)))") (("1" (case-replace "convergence_sequences.convergent?(LAMBDA (i:nat): mu!1(E!1(i)))") (("1" (lemma "convergence_sequences.limit_def" ("v" "LAMBDA (i: nat): mu!1(E!1(i))" "l" "mu!1(IIntersection(E!1))")) (("1" (assert) (("1" (lemma "convergence_sequences.limit_def" ("v" "LAMBDA (i: nat): nu!1(E!1(i))" "l" "nu!1(IIntersection(E!1))")) (("1" (assert) (("1" (lemma "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) (("1" (lemma "cnv_seq_const" ("a" "0")) (("1" (expand "const_fun") (("1" (case-replace "(LAMBDA (x: nat): nu!1(E!1(x)) - mu!1(E!1(x)))=(LAMBDA (x: nat): 0)") (("1" (lemma "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" (apply-extensionality :hide? t) (("1" (inst -18 "E!1(x!2)") (("1" (assert) nil nil) ("2" (inst - "x!2") (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (inst - "x!2") (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil) ("3" (skosimp) (("3" (inst - "i!1") (("3" (flatten) (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil) ("3" (skosimp) (("3" (inst - "i!1") (("3" (flatten) (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil) ("3" (skosimp) (("3" (inst - "i!1") (("3" (flatten) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -8) (("2" (split) (("1" (skosimp) (("1" (assert) nil nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "to_measure[T, (generated_sigma_algebra(C))](nu!1)") (("2" (expand "measure?") (("2" (expand "to_measure") (("2" (expand "measure_empty?") (("2" (flatten) (("2" (assert) (("2" (expand "measure_countably_additive?") (("2" (skosimp) (("2" (typepred "X!1") (("2" (expand "o ") (("2" (inst - "X!1") (("2" (split) (("1" (skosimp) (("1" (assert) (("1" (typepred "X!1(x1!1)") (("1" (expand "S") (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "disjoint_indexed_measurable?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (expand "measurable_set?") (("2" (inst - "x1!1") (("2" (flatten) nil nil)) nil)) nil)) nil) ("3" (replace -7) (("3" (split) (("1" (skosimp) (("1" (assert) nil nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "to_measure[T, (generated_sigma_algebra(C))](mu!1)") (("2" (expand "to_measure") (("2" (expand "measure?") (("2" (expand "measure_empty?") (("2" (flatten) (("2" (assert) (("2" (expand "measure_countably_additive?") (("2" (skosimp) (("2" (typepred "X!1") (("2" (expand "o ") (("2" (inst - "X!1") (("2" (split) (("1" (skosimp) (("1" (typepred "X!1(x1!1)") (("1" (expand "S") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (expand "disjoint_indexed_measurable?") (("2" (propax) 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" (inst - "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" (lemma "generated_subset_algebra_subset1" ("X" "C")) (("2" (lemma "generated_sigma_algebra_subset2" ("X" "C" "Y" "generated_sigma_algebra(generated_subset_algebra(C))")) (("2" (assert) (("2" (split -1) (("1" (lemma "generated_sigma_algebra_subset2" ("X" "generated_subset_algebra(C)" "Y" "generated_sigma_algebra(C)")) (("1" (assert) (("1" (split -1) (("1" (apply-extensionality :hide? t) (("1" (expand "subset?") (("1" (inst - "x!2") (("1" (inst - "x!2") (("1" (expand "member") (("1" (name-replace "LHS" "generated_sigma_algebra(generated_subset_algebra(C))(x!2)") (("1" (name-replace "RHS" "generated_sigma_algebra(C)(x!2)") (("1" (hide -3) (("1" (assert) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (hide-all-but 1) (("2" (lemma "sigma_algebra_is_subset_algebra[T]") (("2" (inst - "generated_sigma_algebra(C)") (("2" (lemma "generated_subset_algebra_subset2[T]" ("X" "C" "Y" "generated_sigma_algebra[T](C)")) (("2" (assert) (("2" (hide -1 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" (skosimp) (("2" (expand "member") (("2" (inst - "x!2") (("2" (assert) (("2" (lemma "generated_sigma_algebra_subset1" ("X" "generated_subset_algebra(C)")) (("2" (expand "subset?") (("2" (inst - "x!2") (("2" (expand "member") (("2" (propax) 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) ((mu_fin? const-decl "bool" measure_props nil) (m_decreasing_convergence formula-decl nil measure_props nil) (limit_lemma formula-decl nil convergence_sequences "analysis/") (cnv_seq_diff formula-decl nil convergence_ops "analysis/") (cnv_seq_const formula-decl nil convergence_ops "analysis/") (unique_limit formula-decl nil convergence_sequences "analysis/") (const_fun const-decl "[T -> real]" real_fun_ops "reals/") (x_converges? const-decl "bool" extended_nnreal "extended_nnreal/") (extended_nnreal nonempty-type-eq-decl nil extended_nnreal "extended_nnreal/") (measurable_set nonempty-type-eq-decl nil measure_space_def nil) (measurable_set? const-decl "bool" measure_space_def nil) (m_increasing_convergence formula-decl nil measure_props nil) (limit_def formula-decl nil convergence_sequences "analysis/") (finite_emptyset name-judgement "finite_set" finite_sets nil) (T_low type-eq-decl nil sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (sigma_eq formula-decl nil sigma "reals/") (sequence type-eq-decl nil sequences nil) (fullset const-decl "set" sets nil) (subset? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (setofsets type-eq-decl nil sets nil) (set type-eq-decl nil sets nil) (nonempty? const-decl "bool" sets nil)) shostak)))
¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.183Bemerkung: (vorverarbeitet am 2026-04-26) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-05-26