|
(complete_measure_theory
(IMP_measure_theory_TCC1 0
(IMP_measure_theory_TCC1-1 nil 3458543745
("" (typepred "mu")
(("" (expand "complete_measure?") (("" (flatten) nil nil)) nil))
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 complete_measure_theory nil)
(setof type-eq-decl nil defined_types nil)
(setofsets type-eq-decl nil sets nil)
(sigma_algebra? const-decl "bool" subset_algebra_def nil)
(sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
(S formal-const-decl "sigma_algebra" complete_measure_theory 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)
(extended_nnreal nonempty-type-eq-decl nil extended_nnreal
"extended_nnreal/")
(complete_measure? const-decl "bool" generalized_measure_def nil)
(complete_measure nonempty-type-eq-decl nil generalized_measure_def
nil)
(mu formal-const-decl "complete_measure" complete_measure_theory
nil))
nil))
(null_subset 0
(null_subset-1 nil 3410757087
("" (skosimp)
(("" (typepred "N!1")
(("" (expand "null_set?")
(("" (typepred "mu")
(("" (expand "complete_measure?")
(("" (flatten)
(("" (expand "measure_complete?")
(("" (expand "measurable_set?")
(("" (expand "mu_fin?")
(("" (expand "mu")
(("" (inst - "X!1" "N!1")
(("" (assert)
(("" (split -2)
(("1"
(lemma "m_monotone"
("a" "X!1" "b" "N!1"))
(("1"
(expand "x_le")
(("1"
(flatten)
(("1" (assert) nil nil))
nil))
nil)
("2"
(expand "measurable_set?")
(("2" (propax) nil nil))
nil)
("3"
(expand "measurable_set?")
(("3" (propax) nil nil))
nil))
nil)
("2" (hide 2)
(("2" (decompose-equality) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((null_set nonempty-type-eq-decl nil measure_theory nil)
(null_set? const-decl "bool" measure_theory nil)
(mu formal-const-decl "complete_measure" complete_measure_theory
nil)
(complete_measure nonempty-type-eq-decl nil generalized_measure_def
nil)
(complete_measure? const-decl "bool" generalized_measure_def nil)
(extended_nnreal nonempty-type-eq-decl nil extended_nnreal
"extended_nnreal/")
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(S formal-const-decl "sigma_algebra" complete_measure_theory nil)
(sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
(sigma_algebra? const-decl "bool" subset_algebra_def nil)
(setofsets type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(set type-eq-decl nil sets nil)
(T formal-type-decl nil complete_measure_theory nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(measurable_set? const-decl "bool" measure_space_def nil)
(mu const-decl "nnreal" measure_props nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(TRUE const-decl "bool" booleans nil)
(m_monotone formula-decl nil measure_props nil)
(measurable_set nonempty-type-eq-decl nil measure_space_def nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(x_le const-decl "bool" extended_nnreal "extended_nnreal/")
(mu_fin? const-decl "bool" measure_props nil)
(measure_complete? const-decl "bool" generalized_measure_def nil))
shostak))
(null_is_negligible 0
(null_is_negligible-1 nil 3410757337
("" (skosimp)
(("" (split)
(("1" (flatten) (("1" (rewrite "null_is_negligible") nil nil))
nil)
("2" (flatten)
(("2" (expand "negligible_set?")
(("2" (skosimp)
(("2" (lemma "null_subset" ("X" "X!1" "N" "X!2"))
(("1" (assert) nil nil) ("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((null_is_negligible judgement-tcc nil measure_theory nil)
(set type-eq-decl nil sets nil)
(null_set? const-decl "bool" measure_theory nil)
(null_set nonempty-type-eq-decl nil measure_theory nil)
(T formal-type-decl nil complete_measure_theory nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(setof type-eq-decl nil defined_types nil)
(setofsets type-eq-decl nil sets nil)
(sigma_algebra? const-decl "bool" subset_algebra_def nil)
(sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
(S formal-const-decl "sigma_algebra" complete_measure_theory 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)
(extended_nnreal nonempty-type-eq-decl nil extended_nnreal
"extended_nnreal/")
(complete_measure? const-decl "bool" generalized_measure_def nil)
(complete_measure nonempty-type-eq-decl nil generalized_measure_def
nil)
(mu formal-const-decl "complete_measure" complete_measure_theory
nil)
(negligible_set? const-decl "bool" measure_theory nil)
(null_subset formula-decl nil complete_measure_theory nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil))
shostak))
(ae_eq_measurable 0
(ae_eq_measurable-1 nil 3410756105
("" (skosimp)
(("" (typepred "g!1")
(("" (expand "ae_eq?")
(("" (expand "restrict")
(("" (expand "pointwise_ae?")
(("" (expand "ae?")
(("" (expand "fullset")
(("" (expand "ae_in?")
(("" (skosimp)
(("" (typepred "E!1")
(("" (expand "negligible_set?")
(("" (skosimp)
(("" (rewrite "measurable_gt")
(("" (rewrite "measurable_gt")
((""
(skosimp)
((""
(inst - "c!1")
((""
(name "AA" "{z: T | g!1(z) > c!1}")
((""
(replace -1)
((""
(name
"BB"
"{z: T | f!1(z) > c!1}")
((""
(replace -1)
((""
(case
"subset?(difference(AA,BB),X!1)")
(("1"
(case
"subset?(difference(BB, AA), X!1)")
(("1"
(case
"BB=union(difference(AA,difference(AA,BB)),difference(BB,AA))")
(("1"
(replace -1 1)
(("1"
(hide -1)
(("1"
(name-replace
"D1"
"difference(BB, AA)")
(("1"
(name-replace
"D2"
"difference(AA, BB)")
(("1"
(lemma
"null_subset"
("X"
"D1"
"N"
"X!1"))
(("1"
(lemma
"null_subset"
("X"
"D2"
"N"
"X!1"))
(("1"
(assert)
(("1"
(expand
"null_set?")
(("1"
(flatten)
(("1"
(lemma
"measurable_difference"
("a"
"AA"
"b"
"D2"))
(("1"
(lemma
"measurable_union"
("a"
"difference[T](AA, D2)"
"b"
"D1"))
(("1"
(expand
"measurable_set?")
(("1"
(propax)
nil
nil))
nil)
("2"
(propax)
nil
nil))
nil)
("2"
(expand
"measurable_set?")
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but 1)
(("2"
(apply-extensionality
:hide?
t)
(("2"
(grind)
nil
nil))
nil))
nil))
nil)
("2"
(hide 2 -1 -2 -3 -6)
(("2"
(expand "difference")
(("2"
(expand "subset?")
(("2"
(expand "member")
(("2"
(expand "AA")
(("2"
(expand "BB")
(("2"
(skosimp)
(("2"
(inst
-
"x!1")
(("2"
(inst
-
"x!1")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(expand "difference")
(("2"
(expand "subset?")
(("2"
(expand "member")
(("2"
(skosimp)
(("2"
(expand "BB")
(("2"
(inst
-
"x!1")
(("2"
(assert)
(("2"
(inst
-
"x!1")
(("2"
(assert)
(("2"
(expand
"AA")
(("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)
((measurable_function nonempty-type-eq-decl nil measure_space_def
nil)
(measurable_function? const-decl "bool" measure_space_def nil)
(S formal-const-decl "sigma_algebra" complete_measure_theory nil)
(sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
(sigma_algebra? const-decl "bool" subset_algebra_def nil)
(setofsets type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(T formal-type-decl nil complete_measure_theory nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(restrict const-decl "R" restrict nil)
(ae? const-decl "bool" measure_theory nil)
(ae_in? const-decl "bool" measure_theory nil)
(negligible nonempty-type-eq-decl nil measure_theory nil)
(negligible_set? const-decl "bool" measure_theory nil)
(mu formal-const-decl "complete_measure" complete_measure_theory
nil)
(complete_measure nonempty-type-eq-decl nil generalized_measure_def
nil)
(complete_measure? const-decl "bool" generalized_measure_def nil)
(extended_nnreal nonempty-type-eq-decl nil extended_nnreal
"extended_nnreal/")
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil) (set type-eq-decl nil sets nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(null_subset formula-decl nil complete_measure_theory nil)
(null_set? const-decl "bool" measure_theory nil)
(null_set nonempty-type-eq-decl nil measure_theory nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(member const-decl "bool" sets nil)
(measurable_union judgement-tcc nil measure_space_def nil)
(measurable_set nonempty-type-eq-decl nil measure_space_def nil)
(measurable_set? const-decl "bool" measure_space_def nil)
(measurable_difference judgement-tcc nil measure_space_def nil)
(union const-decl "set" sets nil)
(BB skolem-const-decl "[T -> bool]" complete_measure_theory nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(TRUE const-decl "bool" booleans nil)
(AA skolem-const-decl "[T -> bool]" complete_measure_theory nil)
(difference const-decl "set" sets nil)
(subset? const-decl "bool" sets nil)
(> const-decl "bool" reals nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(measurable_gt formula-decl nil measure_space_def nil)
(fullset const-decl "set" sets nil)
(pointwise_ae? const-decl "bool" measure_theory nil)
(ae_eq? const-decl "bool" measure_theory nil))
shostak)))
¤ Dauer der Verarbeitung: 0.28 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
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.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
