SSL measure_space_def.prf
Interaktion und
(measure_space_defnil 3357887231"" (expand "measurable_set?" ) (("" (propax) nil nil )) nil )"bool" measure_space_def nil )"(S)" measure_space_defnil )"finite_set[T]" countable_setofsets"sets_aux/" )"finite_set[T]" countable_props"sets_aux/" )"finite_set" finite_sets nil ))nil ))nil 3391152936"" (expand "measurable_set?" ) (("" (propax) nil nil )) nil )"bool" measure_space_def nil )"(S)" measure_space_defnil )"finite_set[T]" countable_setofsets"sets_aux/" )"finite_set[T]" countable_props"sets_aux/" )"finite_set" finite_sets nil ))nil ))nil 3391152936"" (expand "measurable_set?" ) (("" (propax) nil nil )) nil )"bool" measure_space_def nil )"(S)" measure_space_defnil ))nil ))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 )"sigma_algebra" measure_space_def nil )nil subset_algebra_def nil )"bool" subset_algebra_def nil )nil sets nil )nil defined_types nil )"bool" subset_algebra_defnil )"finite_set" finite_sets nil )"finite_set[T]" countable_props"sets_aux/" )"finite_set[T]" countable_setofsets"sets_aux/" )"measurable_set" nil )"(S)" measure_space_defnil )"bool" subset_algebra_def nil )"bool" sets nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil measure_space_def nil )set type-eq-decl nil sets nil )nil measure_space_def nil )"bool" measure_space_def nil ))nil ))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 )"sigma_algebra" measure_space_def nil )nil subset_algebra_def nil )"bool" subset_algebra_def nil )nil sets nil )nil defined_types nil )nil measure_space_def nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"bool" subset_algebra_def nil )"measurable_set" measure_space_def nil )nil measure_space_def nil )"bool" measure_space_def nil )set type-eq-decl nil sets nil )"measurable_set" measure_space_def nil )"bool" sets nil )nil nil ))nil ))nil 3509948250"" (skosimp)"" (typepred "a!1" )"" (typepred "b!1" )"" (lemma "measurable_complement" ("a" "a!1" ))"" (lemma "measurable_complement" ("a" "b!1" ))"" "measurable_union" "a" "complement[T](a!1)" "b" "complement[T](b!1)" ))"" (rewrite "demorgan2" -1 :dir rl)"" "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 )nil measure_space_def nil )"bool" measure_space_def nil )set type-eq-decl nil sets nil )nil measure_space_def nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil measure_space_def nil )"measurable_set" nil )nil measure_space_def nil )"set" sets nil )"set" sets nil )nil sets_lemmas nil )nil sets_lemmas nil ))nil ))nil 3509948250"" (skosimp)"" (rewrite "difference_intersection" )"" (typepred "a!1" )"" (typepred "b!1" )"" (lemma "measurable_complement" ("a" "b!1" ))"" "measurable_intersection" "a" "a!1" "b" "complement(b!1)" ))"" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )nil sets_lemmas nil )nil booleans nil )nil booleans nil )set type-eq-decl nil sets nil )"bool" measure_space_def nil )nil measure_space_def nil )nil measure_space_def nil )"measurable_set" nil )"measurable_set" nil )nil measure_space_def nil )"set" sets nil )nil measure_space_def nil )NOT const-decl "[bool -> bool]" booleans nil ))nil ))nil 3391152936 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil measure_space_def nil )nil defined_types nil )nil sets nil )"bool" subset_algebra_def nil )nil subset_algebra_def nil )"sigma_algebra" measure_space_def nil )set type-eq-decl nil sets nil )"bool" countability "sets_aux/" )nil countability "sets_aux/" )"bool" functions nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil ))nil ))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" "{x: T | LAMBDA (t: setof[T]):IF (S)(t) THEN M!1(t) ELSE FALSE ENDIF)):") "1" (assert ) nil nil )"2" (hide-all-but 1)"2" (apply-extensionality :hide? t)"2" "EXISTS (a: (M!1)): a(x!1)" )"1" "1" "a!1" )"1" (inst + "a!1" ) nil nil ))nil ))nil )"2" replace 1 2)"2" assert )"2" "2" "a!1" )"2" "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" "f!1" )"2" "1" "1" "1" (grind) nil nil ))nil ))nil )"2" expand "injective?" )"2" "2" "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 )nil countability "sets_aux/" )"bool" countability "sets_aux/" )set type-eq-decl nil sets nil )"sigma_algebra" measure_space_def nil )nil subset_algebra_def nil )"bool" subset_algebra_def nil )nil sets nil )nil defined_types nil )nil measure_space_def nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"bool" measure_space_def nil )"R" extend nil )"bool" booleans nil )"(surjective?[setofsets[T], set[T]])" sets_lemmas nil )"bool" functions nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )"(injective?[(M!1), nat])" measure_space_defnil )IF const-decl "[boolean, T, T -> T]" if_def nil )"[T, T -> boolean]" equalities nil )"bool" sets nil )"[bool, bool -> bool]" booleans nil )"(LAMBDA (t: setof[T]): IF (S)(t) THEN M!1(t) ELSE FALSE ENDIF)" nil )"countable_set[(S)]" measure_space_def nil )"set" sets nil )"bool" subset_algebra_def nil ))nil ))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" "measurable_complement" "a" "{x: T | EXISTS (a: (MC)): a(x)}" ))"1" (expand "Intersection" )"1" "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" "FORALL (a: (M!1)): a(x!1)" )"1" (expand "complement" )"1" (expand "member" )"1" "1" "a!1" )"1" expand "MC" )"1" "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" "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" "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 )"set" sets nil )nil countability "sets_aux/" )"bool" countability "sets_aux/" )set type-eq-decl nil sets nil )"[T, T -> boolean]" equalities nil )"sigma_algebra" measure_space_def nil )nil subset_algebra_def nil )"bool" subset_algebra_def nil )nil sets nil )nil defined_types nil )nil booleans nil )nil booleans nil )nil measure_space_def nil )"(S)" nil )"bool" functions nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil sets_lemmas nil )"(injective?[(M!1), nat])" measure_space_defnil )nil measure_space_def nil )nil measure_space_def nil )"bool" measure_space_def nil )nil measure_space_def nil )nil sets_lemmas nil )"(M!1)" measure_space_def nil )"bool" sets nil )NOT const-decl "[bool -> bool]" booleans nil )"countable_set[(S)]" measure_space_def nil )"(MC)" measure_space_def nil )"[(S) -> bool]" measure_space_def nil )"set" sets nil )"set" sets nil ))nil ))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" "{x: T | ") "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" "2" expand "IUnion" )"2" "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" "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 )"set" sets nil )nil sequences nil )"set[R]" function_image nil )nil measure_space_def nil )"bool" measure_space_def nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil countability "sets_aux/" )"bool" countability "sets_aux/" )set type-eq-decl nil sets nil )"sigma_algebra" measure_space_def nil )nil subset_algebra_def nil )"bool" subset_algebra_def nil )nil sets nil )nil defined_types nil )nil booleans nil )nil booleans nil )nil measure_space_def nil )nil measure_space_def nil )"[bool, bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"set" sets nil )"nat" measure_space_def nil )"sequence[measurable_set]" nil )NOT const-decl "[bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )"bool" booleans nil )"set[T]" indexed_sets nil )"set[R]" function_image nil )"bool" functions nil )nil countable_image "sets_aux/" ))nil ))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" "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 )nil measure_space_def nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil sequences nil )nil measure_space_def nil )"bool" measure_space_def nil )set type-eq-decl nil sets nil )nil indexed_sets_aux "sets_aux/" )"measurable_set" nil )nil measure_space_def nil )"set[T]" indexed_sets nil )"set" sets nil )nil measure_space_def nil )nil sets_lemmas nil )"set[T]" indexed_sets_aux "sets_aux/" ))nil ))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 )"set[D]" function_image nil )nil borel nil )"sigma_algebra" borel nil )"setofsets[T]" metric_space_def"metric_space/" )"[numfield, numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )"bool" reals nil )nil subset_algebra_def nil )"bool" subset_algebra_def nil )nil sets nil )nil defined_types nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"set" sets nil )nil sigma_algebra nil )nil sigma_algebra nil )nil measure_space_def nil )"sigma_algebra" measure_space_def nil )"set" sets nil )"bool" sets nil )"bool" measure_space_def nil )"bool" measure_space_def nil ))nil ))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" )"" "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 )"bool" measure_space_def nil )"set[D]" function_image nil )"bool" sets nil )"[S -> T]" const_fun_def "structures/" )nil sigma_algebra nil )"set" sets nil )nil borel nil )"sigma_algebra" borel nil )"setofsets[T]" metric_space_def"metric_space/" )"[numfield, numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )"bool" reals nil )"set" sets nil )"sigma_algebra" measure_space_def nil )nil subset_algebra_def nil )"bool" subset_algebra_def nil )nil sets nil )nil defined_types nil )nil sigma_algebra nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil measure_space_def nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" const_fun_def "structures/" )"bool" measure_space_def nil ))nil ))nil 3357903823"" (skosimp*)"" (split)"1" (flatten)"1" (skosimp)"1" (typepred "X!1" )"1" (expand "measurable_function?" )"1" "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" "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" "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" "extensionality" "f" "emptyset[T]" "g" "inverse_image(f!1, emptyset[real])" ))"1" "1" (assert ) nil nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "subset_algebra_complement?" )"2" (skosimp)"2" (expand "member" )"2" expand "C" )"2" "x!1" )"2" expand "C" )"2" "inverse_image[T,real](f!1,x!1)" )"2" "extensionality" "f" "complement(inverse_image[T,real](f!1, x!1))" "g" "inverse_image(f!1, complement[real](x!1))" ))"2" "1" (assert ) nil nil )"2" "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" "XX" "{W:set[T] | EXISTS (x:(X!1)): W = inverse_image(f!1, x)}" )"3" "XX" )"3" "1" "extensionality" "f" "Union(XX)" "g" "inverse_image(f!1, Union(X!1))" ))"1" "1" (assert ) nil nil )"2" "2" "2" expand "XX" )"2" expand "inverse_image" )"2" expand "member" )"2" expand "Union" )"2" "EXISTS (a: (X!1)): a(f!1(x!1))" )"1" "1" "lambda x: a!1(f!1(x))" )"1" "a!1" )nil nil ))nil ))nil )"2" replace 1 2)"2" assert )"2" "2" "a!1" )"2" "2" replace "2" assert )"2" "x!2" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "XX" )"2" "extensionality" "f" "{W: set[T] | " "g" "image(inverse_image(f!1),X!1)" ))"2" "1" replace -1)"1" "1" "countable_image[set[real],set[T]]" "S" "X!1" "f" "inverse_image(f!1)" ))"1" assert )"1" expand "image" "1" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "image" )"2" expand "inverse_image" )"2" expand "inverse_image" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "x!1" )"3" expand "XX" )"3" "3" "x!2" )"3" "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 )"bool" measure_space_def nil )"(U!1)" measure_space_def nil )"setofsets[real]" measure_space_def nil )"sigma_algebra" borel nil )"setofsets[T]" metric_space_def"metric_space/" )"[numfield, numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )"bool" reals nil )nil subset_algebra_def nil )"bool" subset_algebra_def nil )nil borel nil )"bool" measure_space_def nil )"bool" sets nil )"bool" sets nil )nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil defined_types nil )nil sets nil )"set[D]" function_image nil )"sigma_algebra" measure_space_def nil )nil measure_space_def nil )"[T, T -> boolean]" equalities nil )set type-eq-decl nil sets nil )"set[real]" measure_space_def nil )"(partial_order?[set[T]])" nil )"set" sets nil )"[set[real] -> bool]" measure_space_def nil )"sigma_algebra" nil )nil nil )"bool" subset_algebra_def nil )"(surjective?[setofsets[T], set[T]])" sets_lemmas nil )"(X!1)" measure_space_def nil )"setofsets[real]" measure_space_def nil )"[set[T] -> boolean]" measure_space_def nil )"set" sets nil )"set[R]" function_image nil )nil countable_image "sets_aux/" )"set[D]" function_image nil )"set[R]" function_image nil )"bool" subset_algebra_defnil )"(S)" nil )"[T -> real]" measure_space_def nil )"(C)" measure_space_def nil )"set" sets nil )"bool" subset_algebra_def nil )"measurable_set" nil )"(S)" measure_space_defnil )"real" reals nil )"set" sets nil )nil functions nil )"compact[real, (metric_induced_topology)]" real_topology"metric_space/" )"clopen[real, (metric_induced_topology)]" real_topology"metric_space/" )"(S)" measure_space_defnil )"finite_set[T]" countable_setofsets"sets_aux/" )"finite_set[T]" countable_props"sets_aux/" )"finite_set" finite_sets nil ))nil 3357907013"" (skosimp)"" "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 )nil measure_space_def nil )"set" sets nil )"R" extend nil )"bool" booleans nil )nil real_topology"metric_space/" )"set[T]" metric_space_def "metric_space/" )"[numfield, numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil ) (set type-eq-decl nil sets nil )nil sets nil )nil defined_types nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil measure_space_def nil )"(extend[setof[real], open_interval, bool, FALSE](fullset[open_interval]))" nil )NOT const-decl "[bool -> bool]" booleans nil )"open_interval" measure_space_def nil )nil real_borel nil ))nil 3357918570"" (skosimp)"" (rewrite "measurable_def2" )"" (split)"1" (skosimp*)"1" (typepred "S" )"1" (name "F" "lambda (pn:posnat): ball(c!1+pn,1)" )"1" "VV" "image[posnat,set[real]](F,fullset[posnat])" )"1" "({z | f!1(z) > c!1}) = inverse_image(f!1, Union(VV))" )"1" (hide -1)"1" (rewrite "inverse_image_Union" )"1" "{y: set[T] | EXISTS (x: (VV)): y = inverse_image(f!1, x)} = image(inverse_image(f!1),VV)" )"1" (hide -1)"1" "countable_image[posnat, set[real]]" "f" "F" "S" "fullset[posnat]" ))"1" (split -1)"1" expand "image" -1)"1" replace -2)"1" "countable_image[set[real],set[T]]" "f" "inverse_image(f!1)" ))"1" "VV" )"1" assert )"1" expand "image" -1)"1" expand "sigma_algebra?" )"1" "1" expand "sigma_algebra_union?" )"1" "image(inverse_image(f!1), VV)" )"1" assert )"1" "1" "x!1" )"1" expand "image" "1" expand "inverse_image" )"1" expand "inverse_image" )"1" expand "member" )"1" "1" "x!2" )"1" expand "VV" )"1" expand "fullset" )"1" expand "image" )"1" "1" replace "1" expand "F" "1" "ball(c!1 + x!3, 1)" )"1" assert )nil nil )"2" "c!1+x!3" "1" )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" "2" expand "fullset" )"2" expand "is_countable" )"2" "lambda (n:posnat): n-1" )"2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (apply-extensionality :hide? t)"2" (expand "VV" )"2" expand "fullset" )"2" expand "inverse_image" )"2" expand "member" )"2" expand "image" )"2" expand "inverse_image" )"2" expand "member" )"2" "(EXISTS (x: (VV)): x!1 = ({x_1: T | x(f!1(x_1))}))" )"1" "1" "x!2" )"1" expand "VV" )"1" expand "fullset" )"1" expand "image" )"1" "1" replace -1)"1" "F(x!3)" )"1" "x!3" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace 1 2)"2" assert )"2" "2" "x!2" )"2" "2" "x!2" )"2" expand "VV" )"2" expand "fullset" )"2" expand "image" )"2" "x!3" )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-all-but 1)"2" (apply-extensionality :hide? t)"2" (expand "VV" )"2" (expand "fullset" )"2" (expand "image" )"2" (expand "Union" )"2" expand "inverse_image" )"2" expand "member" )"2" "f!1(x!1) > c!1" )"1" "PN" "ceiling(f!1(x!1)-c!1)" )"1" "ceiling(f!1(x!1) - c!1)" )"1" replace -3)"1" "1" "ball(c!1+PN,1)" )"1" expand "ball" )"1" (grind) nil nil ))nil )"2" expand "F" 1)"2" "PN" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" "a!1" )"2" "2" replace -1)"2" expand "F" )"2" expand "ball" )"2" "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 )"2" (skosimp*)"2" (typepred "S" )"2" (typepred "i!1" )"2" (skosimp)"2" "F" "lambda (pn:posnat): {y:T| x!1-r!1< f!1(y) & f!1(y)<=x!1+r!1-1/pn}" )"2" "inverse_image(f!1, i!1)=Union(image(F,fullset[posnat]))" )"1" (hide -1 -2)"1" (expand "sigma_algebra?" )"1" (flatten)"1" (expand "sigma_algebra_union?" )"1" (inst - "image(F, fullset[posnat])" )"1" "1" (assert ) nil nil )"2" "2" "countable_image[posnat,set[T]]" "f" "F" ))"2" "fullset[posnat]" )"2" "1" expand "image" -1)"1" (propax) nil nil ))nil )"2" "2" expand "fullset" )"2" expand "is_countable" )"2" "lambda (n:posnat): n-1" )"2" expand "injective?" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "x!2" )"3" expand "fullset" )"3" expand "image" )"3" "3" replace -1)"3" expand "F" )"3" assert )"3" "3" "x!1-r!1" )"3" "x!1+r!1-1/x!3" )"3" "sigma_algebra_difference" "x" "{z | f!1(z) > x!1 - r!1}" "y" "{z | f!1(z) > x!1 + r!1 - 1 / x!3}" ))"1" expand "difference" )"1" expand "member" )"1" "{x: T | f!1(x) > x!1 - r!1 AND NOT f!1(x) > r!1 - 1 / x!3 + x!1} = {y: T | x!1 - r!1 < f!1(y) & f!1(y) <= r!1 - 1 / x!3 + x!1}" )"1" "1" "1" "f!1(x!4) > x!1 - r!1" )"1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -1 2)"2" (expand "fullset" )"2" (expand "image" )"2" (expand "Union" )"2" (expand "inverse_image" )"2" "2" "i!1(f!1(x!2))" )"1" replace -2 -1)"1" expand "ball" )"1" "1" "1" "archimedean" "px" "r!1-abs(x!1 - f!1(x!2))" ))"1" "1" "F(n!1)" )"1" expand "F" )"1" nil nil ))nil )"2" "n!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" "a!1" )"2" "2" replace -1)"2" expand "F" )"2" "2" replace -4)"2" "2" expand "ball" )"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 ))nil ))nil ))nil )nil measure_space_def nil )nil measure_space_def nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"real" reals nil )"posnat" measure_space_def nil )nil real_props nil )"posrat" nil )"[posnat -> [T -> boolean]]" measure_space_defnil )"set" sets nil )"odd_int" integers nil )nil sigma_algebra nil )"[numfield, numfield -> numfield]" number_fields nil )"set[T]" metric_space_def "metric_space/" )"[numfield, numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )nil real_types nil )"[T, T -> boolean]" equalities nil )set type-eq-decl nil sets nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"real" reals nil )"real" reals nil )"set" sets nil )"set[D]" function_image nil )nil inverse_image_Union"sets_aux/" )"(surjective?[setofsets[T], set[T]])" sets_lemmas nil )"({y: set[real] | EXISTS (x_1: ({x | TRUE})): y = F(x_1)})" nil )"({x | TRUE})" measure_space_def nil )"set[set[real]]" measure_space_def nil )"real" measure_space_def nil )"bool" booleans nil )"({x | TRUE})" measure_space_def nil )nil real_topology"metric_space/" )"[posnat -> set[real]]" measure_space_def nil )"bool" sets nil )"bool" subset_algebra_def nil )"set[R]" function_image nil )"int" integers nil )"bool" functions nil )nil naturalnumbers nil )"bool" countability "sets_aux/" )nil countable_image "sets_aux/" )"set[D]" function_image nil )"(strict_total_order?[real])" real_props nil )nil integers nil )"bool" reals nil ) (< const-decl "bool" reals nil )"{i | x <= i & i < x + 1}" floor_ceil nil )"[T -> real]" measure_space_def nil )"T" measure_space_def nil )"{i | f!1(x!1) - c!1 <= i & i < 1 + f!1(x!1) - c!1}" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"set" sets nil )"set[R]" function_image nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil defined_types nil )nil sets nil )"bool" subset_algebra_def nil )nil subset_algebra_def nil )"sigma_algebra" measure_space_def nil ))nil 3357918300"" (skosimp)"" (lemma "measurable_gt" ("f" "f!1" ))"" (replace -1)"" (hide -1)"" (typepred "S" )"" (expand "sigma_algebra?" )"" (flatten)"" (expand "subset_algebra_complement?" )"" (split)"1" (skosimp*)"1" (inst - "c!1" )"1" (inst - "{z | f!1(z) > c!1}" )"1" (expand "member" )"1" (expand "complement" )"1" expand "member" )"1" "extensionality" "f" "{x: T | NOT f!1(x) > c!1}" "g" "{z | f!1(z) <= c!1}" ))"1" "1" (assert ) nil nil )"2" "2" "f!1(x!1) <= c!1" )"1" (assert ) nil nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (inst - "c!1" )"2" (inst - "{z | f!1(z) <= c!1}" )"2" (expand "member" )"2" "extensionality" "f" "complement({z | f!1(z) <= c!1})" "g" "{z | f!1(z) > c!1}" ))"2" "1" (assert ) nil nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil measure_space_def nil )nil measure_space_def nil )"bool" subset_algebra_defnil )"real" measure_space_def nil )set type-eq-decl nil sets nil )"real" reals nil )"real" measure_space_def nil )"[T -> real]" measure_space_def nil )"bool" reals nil )"set" sets nil )nil functions nil )"bool" reals nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"bool" sets nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil defined_types nil )nil sets nil )"bool" subset_algebra_def nil )nil subset_algebra_def nil )"sigma_algebra" measure_space_def nil ))nil 3358562291"" (skosimp)"" (split)"1" (flatten)"1" (skosimp)"1" (rewrite "measurable_le" )"1" "VV" "image((lambda (n:posnat): {z | f!1(z) <= c!1-1/n}),fullset[posnat])" )"1" "countable_image[posnat,set[T]]" "f" "(LAMBDA (n: posnat): {z | f!1(z) <= c!1 - 1 / n})" "S" "fullset[posnat]" ))"1" (split -1)"1" (expand "image" -1)"1" (replace -2)"1" (hide -2)"1" "{z_1: T | f!1(z_1) < c!1} = Union(VV)" )"1" (typepred "S" )"1" (expand "sigma_algebra?" )"1" "1" expand "sigma_algebra_union?" )"1" "VV" )"1" assert )"1" "1" "x!1" )"1" expand "VV" )"1" expand "fullset" )"1" expand "image" )"1" "1" "c!1 - 1 / x!2" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (apply-extensionality :hide? t)"2" expand "VV" )"2" expand "fullset" )"2" expand "image" )"2" expand "Union" )"2" "f!1(x!1) < c!1" )"1" "archimedean" "px" "c!1-f!1(x!1)" ))"1" "1" "{z | f!1(z) <= c!1 - 1 /n!1}" )"1" (assert ) nil nil )"2" "n!1" )nil nil ))nil ))nil )"2" (assert ) nil nil ))nil )"2" assert )"2" "2" "a!1" )"2" "2" replace -1)"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (expand "fullset" )"2" (expand "is_countable" )"2" (inst + "lambda (n:posnat): n-1" )"2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (rewrite "measurable_le" )"2" (skosimp)"2" "VV" "image((lambda (n:posnat): {z_1: T | f!1(z_1) >= c!1+1/n}),fullset[posnat])" )"2" (case "subset?(VV,S)" )"1" "countable_image[posnat,set[T]]" "f" "(LAMBDA (n: posnat): {z_1: T | f!1(z_1) >= c!1 + 1 / n})" "S" "fullset[posnat]" ))"1" (expand "image" -1)"1" (replace -3)"1" (split -1)"1" (hide -3)"1" (typepred "S" )"1" (expand "sigma_algebra?" )"1" "1" expand "sigma_algebra_union?" )"1" "VV" )"1" assert )"1" "1" expand "subset_algebra_complement?" )"1" "Union(VV)" )"1" expand "complement" )"1" expand "member" )"1" "extensionality" "f" "{x: T | NOT Union(VV)(x)}" "g" "{z | f!1(z) <= c!1}" ))"1" "1" assert )nil nil )"2" "2" "2" expand "VV" )"2" expand "fullset" )"2" expand "image" )"2" expand "Union" )"2" "f!1(x!1) <= c!1" )"1" "1" "a!1" )"1" "1" replace "1" assert )nil nil ))nil ))nil ))nil ))nil )"2" assert )"2" "archimedean" "px" "f!1(x!1)-c!1" ))"2" "2" "{z_1: T | f!1(z_1) >= 1 /n!1 + c!1}" )"1" assert )nil nil )"2" "n!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "x!1" )"2" expand "subset?" )"2" "x!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (expand "fullset" )"2" (expand "is_countable" )"2" "lambda (n:posnat): n-1" )"2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -1 2)"2" (expand "VV" )"2" (expand "fullset" )"2" (expand "image" )"2" (expand "subset?" )"2" (skosimp)"2" (expand "member" )"2" "2" "S" )"2" expand "sigma_algebra?" )"2" "2" expand "subset_algebra_complement?" )"2" "1 / x!2 + c!1" )"2" "{z_1: T | f!1(z_1) < 1 / x!2 + c!1}" )"2" expand "complement" )"2" expand "member" )"2" "extensionality_postulate" "f" "{x: T | NOT f!1(x) < 1 / x!2 + c!1}" "g" "{z_1: T | f!1(z_1) >= 1 / x!2 + c!1}" ))"2" "2" "2" "1" assert )nil nil )"2" "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 )"set" sets nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )"set[R]" function_image nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"[T, T -> boolean]" equalities nil )set type-eq-decl nil sets nil )nil booleans nil )"real" reals nil )"set" sets nil )nil sets nil )nil defined_types nil )"bool" reals nil )"bool" subset_algebra_def nil )"(surjective?[setofsets[T], set[T]])" sets_lemmas nil )"bool" sets nil )"bool" booleans nil )"set[[T -> bool]]" measure_space_def nil )"sigma_algebra" measure_space_def nil )nil subset_algebra_def nil )"bool" subset_algebra_def nil )NOT const-decl "[bool -> bool]" booleans nil )"(strict_total_order?[real])" real_props nil )nil real_props nil )nil real_types nil )nil real_types nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[T -> real]" measure_space_def nil )"real" measure_space_def nil )"posnat" measure_space_def nil )"(total_order?[real])" nil )"set[R]" function_image nil )"posrat" nil )"int" integers nil )"bool" functions nil )nil naturalnumbers nil )"bool" countability "sets_aux/" )nil countable_image "sets_aux/" )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil measure_space_def nil )nil measure_space_def nil )"[numfield, numfield -> numfield]" number_fields nil )"real" reals nil )nil functions nil )"({x | TRUE})" measure_space_def nil )"(partial_order?[set[T]])" nil )"bool" subset_algebra_defnil )"set" sets nil )nil functions nil )"posnat" measure_space_def nil )"real" measure_space_def nil )"set[[T -> bool]]" measure_space_def nil )"bool" sets nil ))nil 3358565341"" (skosimp)"" (rewrite "measurable_lt" )"" (split)"1" (skosimp*)"1" (inst - "c!1" )"1" "sigma_algebra_complement" "x" "{z | f!1(z) < c!1}" ))"1" (expand "member" )"1" "complement({z | f!1(z) < c!1})={z | f!1(z) >= c!1}" )"1" (apply-extensionality 1 :hide? t)"1" (hide-all-but 1) (("1" (grind) nil nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil )"2" (skosimp*)"2" (inst - "c!1" )"2" "sigma_algebra_complement" "x" "{z | f!1(z) >= c!1}" ))"1" (expand "member" )"1" "complement({z | f!1(z) >= c!1}) = {z | f!1(z) < c!1}" )"1" (apply-extensionality 1 :hide? t)"1" (hide-all-but 1) (("1" (grind) nil nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )nil measure_space_def nil )nil measure_space_def nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"sigma_algebra" measure_space_def nil )nil subset_algebra_def nil )"bool" subset_algebra_def nil )nil sets nil )nil defined_types nil )nil booleans nil )"bool" reals nil )nil sigma_algebra nil )"bool" reals nil )"set" sets nil )"[T, T -> boolean]" equalities nil )set type-eq-decl nil sets nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"(total_order?[real])" nil )"bool" sets nil ))nil 3358597640"" (skosimp)"" (rewrite "measurable_gt" )"" (split)"1" (skosimp*) (("1" (inst - "q!1" ) nil nil )) nil )"2" (skosimp*)"2" (name "Q" "{z:rat| z>c!1}" )"2" (name "F" "lambda (x:real): {z | f!1(z)>x}" )"2" (name "RQ" "{z:real | EXISTS (q:(Q)): q = z}" )"2" (name "FQ" "image(F,RQ)" )"2" (case "Union(FQ) = {z | f!1(z) > c!1}" )"1" (replace -1 * rl)"1" (hide -1)"1" (typepred "S" )"1" (expand "sigma_algebra?" )"1" (flatten)"1" expand "sigma_algebra_union?" )"1" "FQ" )"1" expand "member" )"1" "1" (propax) nil nil )"2" "2" replace -3 * rl)"2" "countable_image[real,set[T]]" )"2" "RQ" "F" )"2" assert )"2" expand "image" -1)"2" "2" "countable_rat" )"2" "2" expand "is_countable" )"2" "lambda (x:(RQ)): f!2(x)" )"1" expand "bijective?" )"1" "1" "1" expand "injective?" )"1" "1" "x1!1" "x2!1" )"1" assert )nil nil )"2" "x2!1" )"2" expand "RQ" )"2" "2" assert )nil nil ))nil ))nil ))nil )"3" "x1!1" )"3" expand "RQ" )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "x!1" )"2" expand "RQ" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "3" "x!1" )"3" expand "FQ" )"3" expand "image" )"3" "3" "x!2" )"3" expand "RQ" )"3" "3" replace "3" expand "F" )"3" "q!1" )"3" assert )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-all-but 1)"2" (apply-extensionality 1 :hide? t)"2" (case-replace "f!1(x!1) > c!1" )"1" (expand "Union" )"1" "density" "x" "c!1" "y" "f!1(x!1)" ))"1" assert )"1" "1" "r!1" )"1" "F(r!1)" )"1" expand "F" )"1" (assert ) nil nil ))nil )"2" expand "FQ" )"2" expand "image" )"2" "r!1" )"2" expand "RQ" )"2" "r!1" )"2" expand "Q" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (replace 1 2)"2" (assert )"2" expand "Union" )"2" "2" "a!1" )"2" expand "FQ" )"2" expand "image" )"2" "2" replace -1)"2" "2" "x!2" )"2" expand "RQ" )"2" "2" "q!1" )"2" replace "2" "2" expand "Q" )"2" expand "F" )"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 measure_space_def nil )nil measure_space_def nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )set type-eq-decl nil sets nil )"set[R]" function_image nil )nil rational_props nil )"rat" measure_space_def nil )"[rat -> bool]" measure_space_def nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"(surjective?[setofsets[T], set[T]])" sets_lemmas nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" subset_algebra_def nil )nil subset_algebra_def nil )"sigma_algebra" measure_space_def nil )"set[R]" function_image nil )nil countable_set "sets_aux/" )"bool" countability "sets_aux/" )"bool" functions nil )"(RQ)" measure_space_def nil )"(RQ)" measure_space_def nil )"[rat -> nat]" measure_space_def nil )"[real -> boolean]" measure_space_def nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" functions nil )nil countable_image "sets_aux/" )"set[[T -> bool]]" measure_space_def nil )"[real -> [T -> bool]]" measure_space_def nil )"bool" sets nil )"bool" subset_algebra_def nil )"set" sets nil )nil sets nil )nil defined_types nil )nil rationals nil )nil booleans nil )"[T, T -> boolean]" equalities nil )"bool" reals nil )nil rationals nil )"[real -> boolean]" rationals nil ))nil 3358671101"" (skosimp)"" (rewrite "measurable_gt2" )"" (typepred "S" )"" (expand "sigma_algebra?" )"" (flatten)"" (hide -1 -3)"" (expand "subset_algebra_complement?" )"" (expand "member" )"" (split)"1" (skosimp*)"1" (inst - "q!1" )"1" (inst - "{z | f!1(z) > q!1}" )"1" "extensionality" "f" "complement({z | f!1(z) > q!1})" "g" "{z | f!1(z) <= q!1}" ))"1" (split -1)"1" (assert ) nil nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (inst - "q!1" )"2" (inst - "{z | f!1(z) <= q!1}" )"2" "extensionality" "f" "{z | f!1(z) > q!1}" "g" "complement({z | f!1(z) <= q!1})" ))"2" (split -1)"1" (assert ) nil nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil measure_space_def nil )nil measure_space_def nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"(S)" nil )"bool" sets nil )"rational" measure_space_def nil )"bool" reals nil )"[T -> real]" measure_space_def nil )"rational" measure_space_def nil )"real" reals nil )"bool" reals nil )"set" sets nil )set type-eq-decl nil sets nil )nil functions nil )"[real -> boolean]" rationals nil )nil rationals nil )"bool" subset_algebra_defnil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil defined_types nil )nil sets nil )"bool" subset_algebra_def nil )nil subset_algebra_def nil )"sigma_algebra" measure_space_def nil ))nil 3358671696"" (skosimp)"" (split)"1" (skosimp*)"1" (rewrite "measurable_lt" ) (("1" (inst - "q!1" ) nil nil ))nil ))nil )"2" (flatten)"2" (rewrite "measurable_lt" )"2" (skosimp)"2" (name "Q" "{q:rat| q<=c!1}" )"2" (name "F" "lambda q: {z|f!1(z)<q}" )"2" (name "FQ" "image(F,Q)" )"2" (typepred "S" )"2" (expand "sigma_algebra?" )"2" (flatten)"2" (hide -1 -2)"2" (expand "sigma_algebra_union?" )"2" (inst - "FQ" )"2" expand "member" )"2" "1" "extensionality" "f" "Union(FQ)" "g" "{z | f!1(z) < c!1}" ))"1" "1" (assert ) nil nil )"2" "2" "2" "f!1(x!1) < c!1" )"1" expand "Union" )"1" "density" "x" "f!1(x!1)" "y" "c!1" ))"1" assert )"1" "1" "F(r!1)" )"1" expand "F" )"1" nil nil ))nil )"2" expand "FQ" )"2" expand "image" )"2" "r!1" )"2" expand "Q" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace 1 2)"2" assert )"2" expand "Union" )"2" "2" "a!1" )"2" expand "FQ" )"2" expand "image" )"2" "2" "x!2" )"2" expand "Q" )"2" replace "2" expand "F" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "countable_image[rat,set[T]]" "f" "F" "S" "Q" ))"2" "1" expand "image" -1)"1" expand "FQ" )"1" (propax) nil nil ))nil ))nil )"2" "2" "countable_full[rat]" )"2" "countable_subset[rat]" "S" "Q" "Count" "fullset[rat]" ))"1" "1" (propax) nil nil )"2" "2" expand "Q" )"2" nil nil ))nil ))nil ))nil )"2" "countably_infinite_type_set[rat]" )"2" assert )"2" "2" expand "fullset" )"2" expand "is_countable" )"2" "countable_rat" )"2" "2" "f!2" )"2" expand "bijective?" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "x!1" )"3" expand "FQ" )"3" expand "image" )"3" "3" replace -1)"3" "3" expand "F" )"3" "x!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 ))nil )nil measure_space_def nil )nil measure_space_def nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil rationals nil )"[real -> boolean]" rationals nil )"bool" reals nil )"[T, T -> boolean]" equalities nil )nil booleans nil )nil rationals nil )set type-eq-decl nil sets nil )"set[R]" function_image nil )"(surjective?[setofsets[T], set[T]])" sets_lemmas nil )"(strict_total_order?[real])" real_props nil )"set[[T -> bool]]" measure_space_def nil )"[rational -> [T -> bool]]" measure_space_defnil )"rat" measure_space_def nil )"(total_order?[real])" nil )"[rat -> bool]" measure_space_def nil )nil rational_props nil )"set" sets nil )nil functions nil )nil countable_image "sets_aux/" )nil countability "sets_aux/" )"bool" countability "sets_aux/" )nil countability "sets_aux/" )"set" sets nil )"real" reals nil )"bool" sets nil )"(partial_order?[set[T]])" nil )nil countable_set "sets_aux/" )"bool" functions nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )"bool" booleans nil )"[rat -> nat]" measure_space_def nil )"bool" functions nil )nil countability"sets_aux/" )nil countability "sets_aux/" )"set[R]" function_image nil )"bool" sets nil )"bool" subset_algebra_def nil )"sigma_algebra" measure_space_def nil )nil subset_algebra_def nil )"bool" subset_algebra_def nil )nil sets nil )nil defined_types nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" reals nil ))nil 3358671342"" (skosimp)"" (typepred "S" )"" (expand "sigma_algebra?" )"" (flatten)"" (hide -1 -3)"" (expand "subset_algebra_complement?" )"" (expand "member" )"" (rewrite "measurable_lt2" )"" (split)"1" (skosimp*)"1" (inst - "q!1" )"1" (inst - "{z | f!1(z) < q!1}" )"1" "extensionality" "f" "complement({z | f!1(z) < q!1})" "g" "{z | f!1(z) >= q!1}" ))"1" (split -1)"1" (assert ) nil nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (inst - "q!1" )"2" (inst - "{z | f!1(z) >= q!1}" )"2" "extensionality" "f" "{z | f!1(z) < q!1}" "g" "complement({z | f!1(z) >= q!1})" ))"2" (split -1)"1" (assert ) nil nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"sigma_algebra" measure_space_def nil )nil subset_algebra_def nil )"bool" subset_algebra_def nil )nil sets nil )nil defined_types nil )nil measure_space_def nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"bool" subset_algebra_defnil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil measure_space_def nil )"rational" measure_space_def nil )"bool" reals nil )"[T -> real]" measure_space_def nil )"rational" measure_space_def nil )"real" reals nil )"bool" reals nil )"set" sets nil )set type-eq-decl nil sets nil )nil functions nil )"[real -> boolean]" rationals nil )nil rationals nil )"bool" sets nil )"(S)" nil ))nil 3357922283"" (skosimp)"" (lemma "trichotomy" ("x" "c!1" ))"" (typepred "g!1" )"" (split -2)"1" (rewrite "measurable_gt" -2)"1" (rewrite "measurable_gt" 1)"1" (skosimp)"1" (inst - "c!2/c!1" )"1" (assert )"1" "extensionality" "f" "{z | g!1(z) > c!2 / c!1}" "g" "{z | (c!1 * g!1)(z) > c!2}" ))"1" (split -1)"1" (assert ) nil nil )"2" (hide -2 2)"2" (skosimp)"2" (assert )"2" expand "*" )"2" assert )"2" "c!1 * g!1(x!1) > c!2" )"1" rewrite "div_mult_pos_gt2" 1)"1" (assert ) nil nil ))nil )"2" replace 1 2)"2" assert )"2" rewrite "div_mult_pos_gt2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (replace -1)"2" (hide-all-but 1)"2" (expand "*" )"2" (lemma "constant_is_measurable" )"2" (inst - "lambda (x:T): 0" )"1" (assert ) nil nil )"2" (expand "constant?" )"2" (inst + "0" )"2" (expand "const_fun" )"2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (rewrite "measurable_gt" 1)"3" (skosimp)"3" (rewrite "measurable_lt" )"3" (inst - "c!2/c!1" )"1" "extensionality" "f" "{z | g!1(z) < c!2/c!1}" "g" "{z | (c!1 * g!1)(z) > c!2}" ))"1" (split -1)"1" (assert ) nil nil )"2" (hide -2 2)"2" (skosimp)"2" (rewrite "div_mult_neg_lt2" 1)"2" (expand "*" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp) (("2" (assert ) nil nil )) nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil real_axioms nil )"[T -> real]" real_fun_ops "reals/" )"real" reals nil )"boolean" notequal nil )"real" measure_space_def nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )nil number_fields nil )nil functions nil )"bool" reals nil )"real" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"(total_order?[real])" nil )nil real_types nil )nil real_types nil )"bool" reals nil )nil extra_real_props nil )"[numfield, numfield -> numfield]" number_fields nil )"(strict_total_order?[real])" real_props nil )nil measure_space_def nil )nil measure_space_def nil )"[S -> T]" const_fun_def "structures/" )"bool" const_fun_def "structures/" )nil real_props nil )"bool" reals nil )nil real_types nil )nil real_types nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"bool" reals nil )nil measure_space_def nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil measure_space_def nil )"bool" measure_space_def nil )nil measure_space_defnil ))nil 3357925399"" (skosimp)"" (typepred "g1!1" )"" (typepred "g2!1" )"" (rewrite "measurable_lt" 1)"" (skosimp)"" (expand "+" 1)"" (rewrite "measurable_lt" -1)"" (rewrite "measurable_lt" -2)"" "F" "lambda q: intersection({z | g1!1(z) < q},{z | g2!1(z) < c!1-q})" )"" "{z | g1!1(z) + g2!1(z) < c!1} = Union(image(F,fullset[rat]))" )"1" (hide -1)"1" "countable_image[rat,set[T]]" "f" "F" ))"1" (inst - "fullset[rat]" )"1" (expand "image" -1)"1" "1" "S" )"1" expand "sigma_algebra?" )"1" "1" expand "sigma_algebra_union?" )"1" "image(F, fullset[rat])" )"1" assert )"1" "1" "1" "x!1" )"1" expand "image" )"1" "1" expand "F" )"1" replace -1)"1" "c!1-x!2" )"1" "x!2" )"1" "sigma_algebra_intersection" "x" "{z | g1!1(z) < x!2}" "y" "{z | g2!1(z) < c!1 - x!2}" ))"1" expand "member" )"1" nil nil ))nil )"2" nil nil )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "countable_type_is_countably_infinite[rat]" )"2" "countable_full[rat]" )"2" assert )"2" "2" expand "is_countable_type" )"2" "countable_rat" )"2" "2" "f!1" )"2" expand "bijective?" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (apply-extensionality :hide? t)"2" "g1!1(x!1) + g2!1(x!1) < c!1" )"1" (expand "Union" )"1" "density" "x" "g1!1(x!1) + g2!1(x!1)" "y" "c!1" ))"1" assert )"1" "1" "r!1" )"1" "density" "x" "g1!1(x!1)" "y" "r!1-g2!1(x!1)" ))"1" assert )"1" "1" "F(r!2)" )"1" expand "F" )"1" expand "intersection" )"1" expand "member" )"1" assert )nil nil ))nil ))nil ))nil )"2" expand "image" )"2" "r!2" )"2" expand "fullset" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (replace 1 2)"2" assert )"2" expand "Union" )"2" "2" "a!1" )"2" expand "image" )"2" "2" replace -1)"2" "x!2" )"2" expand "F" )"2" expand "intersection" )"2" expand "member" )"2" "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 measure_space_defnil )"bool" measure_space_def nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil measure_space_def nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil measure_space_def nil )"[T -> real]" real_fun_ops "reals/" )"real" reals nil )"[numfield, numfield -> numfield]" number_fields nil )nil defined_types nil )nil sets nil )"set" sets nil )"set[R]" function_image nil )nil rationals nil )"set" sets nil )nil countable_image "sets_aux/" )"set[R]" function_image nil )nil countability "sets_aux/" )nil countable_set "sets_aux/" )"bool" functions nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )"[rat -> nat]" measure_space_def nil )"bool" functions nil )"bool" countability "sets_aux/" )nil countability"sets_aux/" )"bool" subset_algebra_def nil )nil subset_algebra_def nil )"sigma_algebra" measure_space_def nil )nil sigma_algebra nil )"[rational -> set[T]]" measure_space_def nil )"bool" sets nil )"(surjective?[setofsets[T], set[T]])" sets_lemmas nil )"bool" subset_algebra_def nil )"(strict_total_order?[real])" real_props nil )"rat" measure_space_def nil )nil rational_props nil )"real" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )set type-eq-decl nil sets nil )"[T, T -> boolean]" equalities nil )"set" sets nil )"bool" reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fieldsnil ))nil 3358645541"" (skosimp)"" (lemma "scal_measurable" ("c" "-1" "g" "g!1" ))"" (expand "*" )"" (expand "-" )"" "extensionality" "f" "LAMBDA (x: T): -1 * g!1(x)" "g" "LAMBDA (x: T): -g!1(x)" ))"" (split -1)"1" (assert ) nil nil )"2" (hide-all-but 1) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )nil measure_space_defnil )"bool" measure_space_def nil )nil booleans nil )nil measure_space_def nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil measure_space_def nil )"odd_int" integers nil )"real" reals nil )"[T -> real]" real_fun_ops "reals/" )"real" reals nil )"[numfield, numfield -> numfield]" number_fields nil )nil functions nil )"[T -> real]" real_fun_ops "reals/" ))nil 3358645494"" (skosimp)"" (lemma "opp_measurable" ("g" "g2!1" ))"" (lemma "sum_measurable" ("g1" "g1!1" "g2" "-g2!1" ))"" (expand "+" )"" (expand "-" ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil )nil measure_space_defnil )"bool" measure_space_def nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil measure_space_def nil )nil measure_space_def nil )"[T -> real]" real_fun_ops "reals/" )"real" reals nil )"real" reals nil )"[T -> real]" real_fun_ops "reals/" )"real" reals nil )"measurable_function" nil )nil measure_space_def nil )"[T -> real]" real_fun_ops "reals/" ))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.201Angebot
(Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können 2026-04-30)
¤ *Eine klare Vorstellung vom Zielzustand
2026-05-26
