| products/sources/formale sprachen/PVS/measure_integration/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: product_sigma_def.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(measure_space_def
(measurable_set_TCC1 0 (measurable_set_TCC1-1 nil 3357887231 ("" (expand "measurable_set?") (("" (propax) nil nil)) nil) ((measurable_set? const-decl "bool" measure_space_def nil) (subset_algebra_emptyset name-judgement "(S)" measure_space_def nil) (finite_emptyset name-judgement "finite_set[T]" countable_setofsets "sets_aux/") (finite_emptyset name-judgement "finite_set[T]" countable_props "sets_aux/") (finite_emptyset name-judgement "finite_set" finite_sets nil)) nil)) (measurable_emptyset 0 (measurable_emptyset-1 nil 3391152936 ("" (expand "measurable_set?") (("" (propax) nil nil)) nil) ((measurable_set? const-decl "bool" measure_space_def nil) (subset_algebra_emptyset name-judgement "(S)" measure_space_def nil) (finite_emptyset name-judgement "finite_set[T]" countable_setofsets "sets_aux/") (finite_emptyset name-judgement "finite_set[T]" countable_props "sets_aux/") (finite_emptyset name-judgement "finite_set" finite_sets nil)) nil)) (measurable_fullset 0 (measurable_fullset-1 nil 3391152936 ("" (expand "measurable_set?") (("" (propax) nil nil)) nil) ((measurable_set? const-decl "bool" measure_space_def nil) (subset_algebra_fullset name-judgement "(S)" measure_space_def nil)) nil)) (measurable_complement 0 (measurable_complement-1 nil 3509948250 ("" (judgement-tcc) (("" (typepred "S") (("" (expand "sigma_algebra?") (("" (expand "subset_algebra_complement?") (("" (flatten) (("" (inst - "a!1") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((S formal-const-decl "sigma_algebra" measure_space_def 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) (subset_algebra_complement? const-decl "bool" subset_algebra_def 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/") (measurable_emptyset name-judgement "measurable_set" measure_space_def nil) (subset_algebra_emptyset name-judgement "(S)" measure_space_def nil) (subset_algebra_empty? const-decl "bool" subset_algebra_def nil) (member 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 measure_space_def nil) (set type-eq-decl nil sets nil) (measurable_set nonempty-type-eq-decl nil measure_space_def nil) (measurable_set? const-decl "bool" measure_space_def nil)) nil)) (measurable_union 0 (measurable_union-1 nil 3509948250 ("" (skosimp) (("" (typepred "S") (("" (lemma "sigma_union_implies_subset_union[T]" ("S" "S")) (("" (expand "sigma_algebra?") (("" (flatten) (("" (expand "subset_algebra_union?") (("" (split) (("1" (inst - "a!1" "b!1") (("1" (assert) (("1" (expand "measurable_set?") (("1" (propax) nil nil)) nil)) nil) ("2" (typepred "b!1") (("2" (expand "measurable_set?") (("2" (propax) nil nil)) nil)) nil) ("3" (typepred "a!1") (("3" (expand "measurable_set?") (("3" (propax) nil nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((S formal-const-decl "sigma_algebra" measure_space_def 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) (T formal-type-decl nil measure_space_def nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (subset_algebra_union? const-decl "bool" subset_algebra_def nil) (a!1 skolem-const-decl "measurable_set" measure_space_def nil) (measurable_set nonempty-type-eq-decl nil measure_space_def nil) (measurable_set? const-decl "bool" measure_space_def nil) (set type-eq-decl nil sets nil) (b!1 skolem-const-decl "measurable_set" measure_space_def nil) (member const-decl "bool" sets nil) (sigma_union_implies_subset_union formula-decl nil subset_algebra_def nil)) nil)) (measurable_intersection 0 (measurable_intersection-1 nil 3509948250 ("" (skosimp) (("" (typepred "a!1") (("" (typepred "b!1") (("" (lemma "measurable_complement" ("a" "a!1")) (("" (lemma "measurable_complement" ("a" "b!1")) (("" (lemma "measurable_union" ("a" "complement[T](a!1)" "b" "complement[T](b!1)")) (("" (rewrite "demorgan2" -1 :dir rl) (("" (lemma "measurable_complement" ("a" "complement(intersection(a!1, b!1))")) (("1" (rewrite "complement_complement") nil nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((measurable_set nonempty-type-eq-decl nil measure_space_def nil) (measurable_set? const-decl "bool" measure_space_def nil) (set type-eq-decl nil sets nil) (T formal-type-decl nil measure_space_def nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (measurable_complement judgement-tcc nil measure_space_def nil) (measurable_complement application-judgement "measurable_set" measure_space_def nil) (measurable_union judgement-tcc nil measure_space_def nil) (complement const-decl "set" sets nil) (intersection const-decl "set" sets nil) (complement_complement formula-decl nil sets_lemmas nil) (demorgan2 formula-decl nil sets_lemmas nil)) nil)) (measurable_difference 0 (measurable_difference-1 nil 3509948250 ("" (skosimp) (("" (rewrite "difference_intersection") (("" (typepred "a!1") (("" (typepred "b!1") (("" (lemma "measurable_complement" ("a" "b!1")) (("" (lemma "measurable_intersection" ("a" "a!1" "b" "complement(b!1)")) (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((difference_intersection formula-decl nil sets_lemmas nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (set type-eq-decl nil sets nil) (measurable_set? const-decl "bool" measure_space_def nil) (measurable_set nonempty-type-eq-decl nil measure_space_def nil) (T formal-type-decl nil measure_space_def nil) (measurable_complement application-judgement "measurable_set" measure_space_def nil) (measurable_intersection application-judgement "measurable_set" measure_space_def nil) (measurable_intersection judgement-tcc nil measure_space_def nil) (complement const-decl "set" sets nil) (measurable_complement judgement-tcc nil measure_space_def nil) (NOT const-decl "[bool -> bool]" booleans nil)) nil)) (measurable_Union_TCC1 0 (measurable_Union_TCC1-1 nil 3391152936 ("" (subtype-tcc) 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 measure_space_def 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" measure_space_def nil) (set type-eq-decl nil sets nil) (is_countable const-decl "bool" countability "sets_aux/") (countable_set nonempty-type-eq-decl nil countability "sets_aux/") (injective? const-decl "bool" functions nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals 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)) nil)) (measurable_Union 0 (measurable_Union-1 nil 3391152936 ("" (skosimp) (("" (typepred "M!1") (("" (typepred "S") (("" (expand "sigma_algebra?") (("" (flatten) (("" (expand "measurable_set?") (("" (expand "sigma_algebra_union?") (("" (inst - "M!1") (("" (split) (("1" (expand "extend") (("1" (expand "Union") (("1" (case-replace "{x: T | EXISTS (a: (LAMBDA (t: setof[T]): IF (S)(t) THEN M!1(t) ELSE FALSE ENDIF)): a(x)}={x: T | EXISTS (a: (M!1)): a(x)}") (("1" (assert) nil nil) ("2" (hide-all-but 1) (("2" (apply-extensionality :hide? t) (("2" (case-replace "EXISTS (a: (M!1)): a(x!1)") (("1" (skosimp) (("1" (typepred "a!1") (("1" (inst + "a!1") nil nil)) nil)) nil) ("2" (replace 1 2) (("2" (assert) (("2" (skosimp) (("2" (inst + "a!1") (("2" (typepred "a!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-3 1)) (("2" (expand "extend") (("2" (expand "is_countable") (("2" (skolem!) (("2" (typepred "f!1") (("2" (inst + "f!1") (("2" (split) (("1" (skosimp) (("1" (hide -1) (("1" (grind) nil nil)) nil)) nil) ("2" (expand "injective?") (("2" (skosimp*) (("2" (inst - "x1!1" "x2!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (typepred "x!1") (("3" (expand "extend") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((countable_set nonempty-type-eq-decl nil countability "sets_aux/") (is_countable const-decl "bool" countability "sets_aux/") (set type-eq-decl nil sets nil) (S formal-const-decl "sigma_algebra" measure_space_def 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) (T formal-type-decl nil measure_space_def 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) (extend const-decl "R" extend nil) (FALSE const-decl "bool" booleans nil) (Union_surjective name-judgement "(surjective?[setofsets[T], set[T]])" sets_lemmas nil) (injective? const-decl "bool" functions nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals 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) (AND const-decl "[bool, bool -> bool]" booleans nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (f!1 skolem-const-decl "(injective?[(M!1), nat])" measure_space_def nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (= const-decl "[T, T -> boolean]" equalities nil) (member const-decl "bool" sets nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (a!1 skolem-const-decl "(LAMBDA (t: setof[T]): IF (S)(t) THEN M!1(t) ELSE FALSE ENDIF)" measure_space_def nil) (M!1 skolem-const-decl "countable_set[(S)]" measure_space_def nil) (Union const-decl "set" sets nil) (sigma_algebra_union? const-decl "bool" subset_algebra_def nil)) nil)) (measurable_Intersection 0 (measurable_Intersection-1 nil 3391152936 ("" (skosimp) (("" (name "MC" "{a:(S)| M!1(complement(a))}") (("" (case "is_countable[(S)](MC)") (("1" (lemma "measurable_Union" ("M" "MC")) (("1" (expand "Union") (("1" (lemma "measurable_complement" ("a" "{x: T | EXISTS (a: (MC)): a(x)}")) (("1" (expand "Intersection") (("1" (case-replace "complement[T]({x: T | EXISTS (a: (MC)): a(x)})={x: T | FORALL (a: (M!1)): a(x)} (("1" (hide-all-but 1) (("1" (apply-extensionality :hide? t) (("1" (case-replace "FORALL (a: (M!1)): a(x!1)") (("1" (case-replace "FORALL (a: (M!1)): a(x!1)") (("1" (expand "complement") (("1" (expand "member") (("1" (skosimp) (("1" (typepred "a!1") (("1" (expand "MC") (("1" (inst - "complement(a!1)") (("1" (expand "complement") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace 1 2) (("2" (assert) (("2" (skosimp) (("2" (expand "complement") (("2" (expand "member") (("2" (inst + "complement(a!1)") (("1" (expand "complement") (("1" (assert) nil nil)) nil) ("2" (expand "MC") (("2" (rewrite "complement_complement") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil) ("2" (propax) nil nil)) nil) ("2" (hide-all-but 1) (("2" (typepred "M!1") (("2" (expand "is_countable") (("2" (skosimp) (("2" (typepred "f!1") (("2" (inst + "lambda (x:(MC)): f!1(complement(x))") (("1" (expand "injective?") (("1" (skosimp) (("1" (inst - "complement[T](x1!1)" "complement[T](x2!1)") (("1" (rewrite "complement_equal") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (typepred "x!1") (("2" (expand "MC") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((complement const-decl "set" sets nil) (countable_set nonempty-type-eq-decl nil countability "sets_aux/") (is_countable const-decl "bool" countability "sets_aux/") (set type-eq-decl nil sets nil) (= const-decl "[T, T -> boolean]" equalities nil) (S formal-const-decl "sigma_algebra" measure_space_def 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) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T formal-type-decl nil measure_space_def nil) (subset_algebra_complement application-judgement "(S)" measure_space_def nil) (injective? const-decl "bool" functions nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals 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) (complement_equal formula-decl nil sets_lemmas nil) (f!1 skolem-const-decl "(injective?[(M!1), nat])" measure_space_def nil) (measurable_Union judgement-tcc nil measure_space_def nil) (measurable_complement judgement-tcc nil measure_space_def nil) (measurable_set? const-decl "bool" measure_space_def nil) (measurable_set nonempty-type-eq-decl nil measure_space_def nil) (complement_complement formula-decl nil sets_lemmas nil) (a!1 skolem-const-decl "(M!1)" measure_space_def nil) (member const-decl "bool" sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (M!1 skolem-const-decl "countable_set[(S)]" measure_space_def nil) (a!1 skolem-const-decl "(MC)" measure_space_def nil) (MC skolem-const-decl "[(S) -> bool]" measure_space_def nil) (Intersection const-decl "set" sets nil) (Union const-decl "set" sets nil)) nil)) (measurable_IUnion 0 (measurable_IUnion-1 nil 3509948250 ("" (skosimp) (("" (lemma "measurable_Union" ("M" "image(SS!1)(fullset[nat])")) (("1" (expand "fullset") (("1" (expand "image") (("1" (expand "image") (("1" (expand "Union") (("1" (case-replace "{x: T | EXISTS (a: ({y: measurable_set | EXISTS (x_1: ({x: nat | TRUE})): y = SS!1(x_1)})): a(x)}=IUnion[nat, T](SS!1)") (("1" (apply-extensionality :hide? t) (("1" (hide -1 2) (("1" (case-replace "IUnion[nat, T](SS!1)(x!1)") (("1" (expand "IUnion") (("1" (skosimp) (("1" (inst + "SS!1(i!1)") (("1" (inst + "i!1") nil nil)) nil)) nil)) nil) ("2" (replace 1 2) (("2" (assert) (("2" (skosimp) (("2" (typepred "a!1") (("2" (skosimp) (("2" (expand "IUnion") (("2" (inst + "x!2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (split) (("1" (expand "measurable_set?") (("1" (propax) nil nil)) nil) ("2" (lemma "countable_image[nat,measurable_set]" ("S" "fullset[nat]" "f" "SS!1")) (("2" (split) (("1" (assert) (("1" (expand "fullset") (("1" (expand "image") (("1" (expand "image") (("1" (expand "is_countable") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "fullset") (("2" (expand "is_countable") (("2" (inst + "lambda (n:nat): n") (("2" (expand "injective?") (("2" (skosimp) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((fullset const-decl "set" sets nil) (sequence type-eq-decl nil sequences nil) (image const-decl "set[R]" function_image nil) (measurable_set nonempty-type-eq-decl nil measure_space_def nil) (measurable_set? const-decl "bool" measure_space_def nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals 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) (countable_set nonempty-type-eq-decl nil countability "sets_aux/") (is_countable const-decl "bool" countability "sets_aux/") (set type-eq-decl nil sets nil) (S formal-const-decl "sigma_algebra" measure_space_def 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) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T formal-type-decl nil measure_space_def nil) (measurable_Union judgement-tcc nil measure_space_def nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (Union const-decl "set" sets nil) (i!1 skolem-const-decl "nat" measure_space_def nil) (SS!1 skolem-const-decl "sequence[measurable_set]" measure_space_def nil) (NOT const-decl "[bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (TRUE const-decl "bool" booleans nil) (IUnion const-decl "set[T]" indexed_sets nil) (image const-decl "set[R]" function_image nil) (injective? const-decl "bool" functions nil) (countable_image formula-decl nil countable_image "sets_aux/")) nil)) (measurable_IIntersection 0 (measurable_IIntersection-1 nil 3509948250 ("" (skosimp) (("" (lemma "IDemorgan2[nat,T]" ("A" "SS!1")) (("" (case "forall (n:nat): measurable_set?(IComplement[nat, T](SS!1)(n))") (("1" (lemma "measurable_IUnion" ("SS" "IComplement(SS!1)")) (("1" (replace -3 -1 rl) (("1" (lemma "measurable_complement" ("a" "complement(IIntersection(SS!1))")) (("1" (rewrite "complement_complement") nil nil) ("2" (propax) nil nil)) nil)) nil) ("2" (propax) nil nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp) (("2" (expand "IComplement") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((T formal-type-decl nil measure_space_def nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals 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) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (sequence type-eq-decl nil sequences nil) (measurable_set nonempty-type-eq-decl nil measure_space_def nil) (measurable_set? const-decl "bool" measure_space_def nil) (set type-eq-decl nil sets nil) (IDemorgan2 formula-decl nil indexed_sets_aux "sets_aux/") (measurable_complement application-judgement "measurable_set" measure_space_def nil) (measurable_IUnion judgement-tcc nil measure_space_def nil) (IIntersection const-decl "set[T]" indexed_sets nil) (complement const-decl "set" sets nil) (measurable_complement judgement-tcc nil measure_space_def nil) (complement_complement formula-decl nil sets_lemmas nil) (IComplement const-decl "set[T]" indexed_sets_aux "sets_aux/")) nil)) (measurable_function_TCC1 0 (measurable_function_TCC1-1 nil 3357887231 ("" (expand "measurable_function?") (("" (skosimp) (("" (expand "measurable_set?") (("" (expand "inverse_image") (("" (expand "member") (("" (typepred "B!1") (("" (case-replace "B!1(0)") (("1" (lemma "sigma_algebra_fullset[T,(S)]") (("1" (expand "member") (("1" (expand "fullset") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (lemma "sigma_algebra_emptyset[T,(S)]") (("2" (expand "member") (("2" (expand "emptyset") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((inverse_image const-decl "set[D]" function_image nil) (borel nonempty-type-eq-decl nil borel nil) (borel? const-decl "sigma_algebra" borel nil) (metric_induced_topology const-decl "setofsets[T]" metric_space_def "metric_space/") (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals 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) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (emptyset const-decl "set" sets nil) (sigma_algebra_emptyset formula-decl nil sigma_algebra nil) (sigma_algebra_fullset formula-decl nil sigma_algebra nil) (T formal-type-decl nil measure_space_def nil) (S formal-const-decl "sigma_algebra" measure_space_def nil) (fullset const-decl "set" sets nil) (member const-decl "bool" sets nil) (measurable_set? const-decl "bool" measure_space_def nil) (measurable_function? const-decl "bool" measure_space_def nil)) nil)) (constant_is_measurable 0 (constant_is_measurable-1 nil 3357888488 ("" (skosimp) (("" (expand "measurable_function?") (("" (skosimp) (("" (expand "inverse_image") (("" (expand "measurable_set?") (("" (expand "member") (("" (typepred "x!1") (("" (expand "constant?") (("" (skosimp) (("" (replace -1) (("" (hide -1) (("" (expand "const_fun") (("" (lemma "sigma_algebra_emptyset[T,S]") (("" (lemma "sigma_algebra_fullset[T,S]") (("" (expand "fullset") (("" (expand "emptyset") (("" (expand "member") (("" (case-replace "B!1(a!1)") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((measurable_function? const-decl "bool" measure_space_def nil) (inverse_image const-decl "set[D]" function_image nil) (member const-decl "bool" sets nil) (const_fun const-decl "[S -> T]" const_fun_def "structures/") (sigma_algebra_fullset formula-decl nil sigma_algebra nil) (emptyset const-decl "set" sets nil) (borel nonempty-type-eq-decl nil borel nil) (borel? const-decl "sigma_algebra" borel nil) (metric_induced_topology const-decl "setofsets[T]" metric_space_def "metric_space/") (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (fullset const-decl "set" sets nil) (S formal-const-decl "sigma_algebra" measure_space_def 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) (sigma_algebra_emptyset formula-decl nil sigma_algebra 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 measure_space_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) (constant? const-decl "bool" const_fun_def "structures/") (measurable_set? const-decl "bool" measure_space_def nil)) nil)) (measurable_def 0 (measurable_def-1 nil 3357903823 ("" (skosimp*) (("" (split) (("1" (flatten) (("1" (skosimp) (("1" (typepred "X!1") (("1" (expand "measurable_function?") (("1" (lemma "generated_sigma_algebra_subset1" ("X" "U!1")) (("1" (replace -4 -1 rl) (("1" (expand "subset?") (("1" (inst - "X!1") (("1" (expand "member") (("1" (inst - "X!1") (("1" (expand "measurable_set?") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (name "C" "{Y| S(inverse_image(f!1,Y))}") (("2" (case "subset?[set[real]](U!1,C)") (("1" (case "sigma_algebra?[real](C)") (("1" (lemma "generated_sigma_algebra_subset2" ("X" "U!1" "Y" "C")) (("1" (assert) (("1" (expand "measurable_function?") (("1" (skosimp) (("1" (typepred "B!1") (("1" (expand "measurable_set?") (("1" (replace -7 -1) (("1" (hide -7) (("1" (expand "generated_sigma_algebra" -1) (("1" (expand "Intersection") (("1" (inst - "C") (("1" (expand "C") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2 -2 -4) (("2" (typepred "S") (("2" (expand "sigma_algebra?") (("2" (flatten) (("2" (split) (("1" (expand "subset_algebra_empty?") (("1" (expand "member") (("1" (expand "C") (("1" (lemma "extensionality" ("f" "emptyset[T]" "g" "inverse_image(f!1, emptyset[real])")) (("1" (split -1) (("1" (assert) nil nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "subset_algebra_complement?") (("2" (skosimp) (("2" (expand "member") (("2" (expand "C") (("2" (typepred "x!1") (("2" (expand "C") (("2" (inst - "inverse_image[T,real](f!1,x!1)") (("2" (lemma "extensionality" ("f" "complement(inverse_image[T,real](f!1, x!1))" "g" "inverse_image(f!1, complement[real](x!1))")) (("2" (split -1) (("1" (assert) nil nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "sigma_algebra_union?") (("3" (skosimp) (("3" (expand "member") (("3" (expand "C") (("3" (name "XX" "{W:set[T] | EXISTS (x:(X!1)): W = inverse_image(f!1, x)}") (("3" (inst -6 "XX") (("3" (split -6) (("1" (lemma "extensionality" ("f" "Union(XX)" "g" "inverse_image(f!1, Union(X!1))")) (("1" (split -1) (("1" (assert) nil nil) ("2" (hide-all-but 1) (("2" (skosimp) (("2" (expand "XX") (("2" (expand "inverse_image") (("2" (expand "member") (("2" (expand "Union") (("2" (case-replace "EXISTS (a: (X!1)): a(f!1(x!1))") (("1" (skosimp) (("1" (inst + "lambda x: a!1(f!1(x))") (("1" (inst + "a!1") nil nil)) nil)) nil) ("2" (replace 1 2) (("2" (assert) (("2" (skosimp) (("2" (typepred "a!1") (("2" (skosimp) (("2" (replace -1) (("2" (assert) (("2" (inst + "x!2") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-2 1)) (("2" (expand "XX") (("2" (lemma "extensionality" ("f" "{W: set[T] | EXISTS (x: (X!1)): W = inverse_image(f!1, x)}" "g" "image(inverse_image(f!1),X!1)")) (("2" (split -1) (("1" (replace -1) (("1" (hide -1) (("1" (lemma "countable_image[set[real],set[T]]" ("S" "X!1" "f" "inverse_image(f!1)")) (("1" (assert) (("1" (expand "image" -1) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp) (("2" (expand "image") (("2" (expand "inverse_image") (("2" (expand "inverse_image") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (typepred "x!1") (("3" (expand "XX") (("3" (skosimp) (("3" (typepred "x!2") (("3" (inst -5 "x!2") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "subset?") (("2" (skosimp) (("2" (expand "member") (("2" (expand "C") (("2" (inst -3 "x!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((measurable_function? const-decl "bool" measure_space_def nil) (X!1 skolem-const-decl "(U!1)" measure_space_def nil) (U!1 skolem-const-decl "setofsets[real]" measure_space_def nil) (borel? const-decl "sigma_algebra" borel nil) (metric_induced_topology const-decl "setofsets[T]" metric_space_def "metric_space/") (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil) (sigma_algebra? const-decl "bool" subset_algebra_def nil) (borel nonempty-type-eq-decl nil borel nil) (measurable_set? const-decl "bool" measure_space_def nil) (member const-decl "bool" sets nil) (subset? const-decl "bool" sets nil) (generated_sigma_algebra_subset1 formula-decl nil subset_algebra_def nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans 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) (setof type-eq-decl nil defined_types nil) (setofsets type-eq-decl nil sets nil) (inverse_image const-decl "set[D]" function_image nil) (S formal-const-decl "sigma_algebra" measure_space_def nil) (T formal-type-decl nil measure_space_def nil) (= const-decl "[T, T -> boolean]" equalities nil) (set type-eq-decl nil sets nil) (x!1 skolem-const-decl "set[real]" measure_space_def nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (Intersection const-decl "set" sets nil) (C skolem-const-decl "[set[real] -> bool]" measure_space_def nil) (generated_sigma_algebra const-decl "sigma_algebra" subset_algebra_def nil) (generated_sigma_algebra_subset2 formula-decl nil subset_algebra_def nil) (sigma_algebra_union? const-decl "bool" subset_algebra_def nil) (Union_surjective name-judgement "(surjective?[setofsets[T], set[T]])" sets_lemmas nil) (a!1 skolem-const-decl "(X!1)" measure_space_def nil) (X!1 skolem-const-decl "setofsets[real]" measure_space_def nil) (XX skolem-const-decl "[set[T] -> boolean]" measure_space_def nil) (Union const-decl "set" sets nil) (image const-decl "set[R]" function_image nil) (countable_image formula-decl nil countable_image "sets_aux/") (inverse_image const-decl "set[D]" function_image nil) (image const-decl "set[R]" function_image nil) (subset_algebra_complement? const-decl "bool" subset_algebra_def nil) (subset_algebra_complement application-judgement "(S)" measure_space_def nil) (f!1 skolem-const-decl "[T -> real]" measure_space_def nil) (x!1 skolem-const-decl "(C)" measure_space_def nil) (complement const-decl "set" sets nil) (subset_algebra_empty? const-decl "bool" subset_algebra_def nil) (measurable_emptyset name-judgement "measurable_set" measure_space_def nil) (subset_algebra_emptyset name-judgement "(S)" measure_space_def nil) (real_minus_real_is_real application-judgement "real" reals nil) (emptyset const-decl "set" sets nil) (extensionality formula-decl nil functions nil) (emptyset_is_compact name-judgement "compact[real, (metric_induced_topology)]" real_topology "metric_space/") (emptyset_is_clopen name-judgement "clopen[real, (metric_induced_topology)]" real_topology "metric_space/") (subset_algebra_emptyset name-judgement "(S)" measure_space_def nil) (finite_emptyset name-judgement "finite_set[T]" countable_setofsets "sets_aux/") (finite_emptyset name-judgement "finite_set[T]" countable_props "sets_aux/") (finite_emptyset name-judgement "finite_set" finite_sets nil)) shostak)) (measurable_def2 0 (measurable_def2-1 nil 3357907013 ("" (skosimp) (("" (lemma "measurable_def" ("f" "f!1" "U" "fullset[open_interval]")) (("" (lemma "borel_generated_by_open_interval") (("" (replace -1 -2 rl) (("" (replace -2 1) (("" (hide-all-but 1) (("" (split) (("1" (skosimp*) (("1" (inst - "i!1") (("1" (expand "fullset") (("1" (expand "extend") (("1" (prop) (("1" (typepred "i!1") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (typepred "X!1") (("2" (expand "fullset") (("2" (expand "extend") (("2" (prop) (("2" (inst - "X!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((T formal-type-decl nil measure_space_def nil) (fullset const-decl "set" sets nil) (extend const-decl "R" extend nil) (FALSE const-decl "bool" booleans nil) (open_interval nonempty-type-eq-decl nil real_topology "metric_space/") (ball const-decl "set[T]" metric_space_def "metric_space/") (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (set type-eq-decl nil sets nil) (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans 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) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (measurable_def formula-decl nil measure_space_def nil) (X!1 skolem-const-decl "(extend[setof[real], open_interval, bool, FALSE](fullset[open_interval]))" measure_space_def nil) (NOT const-decl "[bool -> bool]" booleans nil) (i!1 skolem-const-decl "open_interval" measure_space_def nil) (borel_generated_by_open_interval formula-decl nil real_borel nil)) shostak)) (measurable_gt 0 (measurable_gt-1 nil 3357918570 ("" (skosimp) (("" (rewrite "measurable_def2") (("" (split) (("1" (skosimp*) (("1" (typepred "S") (("1" (name "F" "lambda (pn:posnat): ball(c!1+pn,1)") (("1" (name "VV" "image[posnat,set[real]](F,fullset[posnat])") (("1" (case-replace "({z | f!1(z) > c!1}) = inverse_image(f!1, Union(VV))") (("1" (hide -1) (("1" (rewrite "inverse_image_Union") (("1" (case-replace "{y: set[T] | EXISTS (x: (VV)): y = inverse_image(f!1, x)} = image(inverse_image (("1" (hide -1) (("1" (lemma "countable_image[posnat, set[real]]" ("f" "F" "S" "fullset[posnat]")) (("1" (split -1) (("1" (expand "image" -1) (("1" (replace -2) (("1" (lemma "countable_image[set[real],set[T]]" ("f" "inverse_image(f!1)")) (("1" (inst - "VV") (("1" (assert) (("1" (expand "image" -1) (("1" (expand "sigma_algebra?") (("1" (flatten) (("1" (expand "sigma_algebra_union?") (("1" (inst - "image(inverse_image(f!1), VV)") (("1" (assert) (("1" (skosimp) (("1" (typepred "x!1") (("1" (expand "image" -1) (("1" (expand "inverse_image") (("1" (expand "inverse_image") (("1" (expand "member") (("1" (skosimp) (("1" (typepred "x!2") (("1" (expand "VV") (("1" (expand --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.70 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.Bot Zugriff |
