outer_measure_props.prf
Interaktion und
(outer_measure_propsnil 3396688507"" (typepred "m" )"" (expand "outer_measure?" )"" (flatten)"" (expand "om_empty?" ) (("" (propax) nil nil )) nil )) nil ))nil ))nil )"bool" outer_measure_def nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil outer_measure_props nil )set type-eq-decl nil sets nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil real_types nil )nil extended_nnreal"extended_nnreal/" )"bool" outer_measure_def nil )nil outer_measure_def nil )"outer_measure" outer_measure_props nil ))nil 3396688522"" (typepred "m" )"" (expand "outer_measure?" )"" (flatten)"" (expand "om_increasing?" ) (("" (propax) nil nil )) nil ))nil ))nil ))nil )"bool" outer_measure_def nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil outer_measure_props nil )set type-eq-decl nil sets nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil real_types nil )nil extended_nnreal"extended_nnreal/" )"bool" outer_measure_def nil )nil outer_measure_def nil )"outer_measure" outer_measure_props nil ))nil 3396688484"" (typepred "m" )"" (expand "outer_measure?" )"" (flatten)"" (expand "om_countably_subadditive?" )"" (propax) nil nil )) nil ))nil ))nil ))nil )"bool" outer_measure_def nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil outer_measure_props nil )set type-eq-decl nil sets nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil real_types nil )nil extended_nnreal"extended_nnreal/" )"bool" outer_measure_def nil )nil outer_measure_def nil )"outer_measure" outer_measure_props nil ))nil 3396763601"" (expand "outer_negligible?" )"" (typepred "m" )"" (expand "outer_measure?" )"" (flatten)"" (expand "om_empty?" ) (("" (propax) nil nil )) nil )) nil ))nil ))nil ))nil )"outer_measure" outer_measure_props nil )nil outer_measure_def nil )"bool" outer_measure_def nil )nil extended_nnreal"extended_nnreal/" )nil real_types nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )set type-eq-decl nil sets nil )nil outer_measure_props nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"bool" outer_measure_def nil )"bool" outer_measure_props nil ))nil ))nil 3396585602"" (expand "outer_measurable?" )"" (skosimp*)"" (case-replace "intersection(y!1, emptyset[T])=emptyset[T]" )"1" "intersection(y!1, complement(emptyset[T]))=y!1" )"1" (lemma "m_outer_empty" )"1" (replace -1)"1" (expand "x_add" )"1" (expand "x_eq" )"1" (hide-all-but 1) (("1" (grind) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (apply-extensionality :hide? t)"2" (grind) nil nil )) nil ))nil ))nil )"2" (hide-all-but 1)"2" (apply-extensionality :hide? t) (("2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil )"set" sets nil )"bool" extended_nnreal "extended_nnreal/" )"extended_nnreal" extended_nnreal"extended_nnreal/" )nil outer_measure_props nil )"bool" sets nil )"set" sets nil )"set" sets nil )"[T, T -> boolean]" equalities nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil outer_measure_props nil )"finite_set[T]" "orders/" )"finite_set[T]" bounded_nats"orders/" )"finite_set[T]" countable_props"sets_aux/" )"finite_set" finite_sets nil )"bool" outer_measure_props nil ))nil ))nil 3396787341"" (skosimp*)"" "m_outer_subadditive" "A" "lambda i: if i=0 then intersection(y!1, x!1) elsif i=1 then intersection(y!1, complement(x!1)) else emptyset[T] endif" ))"" "IUnion(LAMBDA i: IF i = 0 THEN intersection(y!1, x!1)") "1" (hide -1)"1" (expand "o" )"1" "x_sum(LAMBDA (i: nat): IF i = 0 THEN m(intersection(y!1, x!1))IF i = 1 THEN m(intersection(y!1, complement(x!1)))") "1" (hide -1 2)"1" (expand "x_sum" )"1" (name-replace "AA" "intersection(y!1, x!1)" )"1" "BB" "intersection(y!1, complement(x!1))" )"1" (lemma "m_outer_empty" )"1" (replace -1)"1" (assert )"1" (expand "x_add" )"1" "m(AA)`1" )"1" "m(BB)`1" )"1" "1" assert )"1" "zero_tail_series_conv" "a" "(LAMBDA (i_1: nat): IF i_1 = 0 THEN m(AA)`2IF i_1 = 1 THEN m(BB)`2 ELSE 0 ENDIF" "n" "1" ))"1" "(FORALL (m_1: nat): LAMBDA (i_1: nat):IF i_1 = 0 THEN m(AA)`2IF i_1 = 1 THEN m(BB)`2 ELSE 0 ENDIF") "1" replace -2)"1" "1" "zero_tail_series_limit" "a" "(LAMBDA (i_1: nat): IF i_1 = 0 THEN m(AA)`2IF i_1 = 1 THEN m(BB)`2 ELSE 0 ENDIF" "n" "1" ))"1" replace -2 -1)"1" replace -1)"1" "1" expand "series" )"1" expand "sigma" )"1" expand "sigma" )"1" expand "sigma" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" assert )"2" "2" "1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" assert )"2" "2" assert )"2" (inst - "0" ) 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 "IUnion" )"2" (expand "intersection" )"2" (expand "complement" )"2" (expand "emptyset" )"2" (expand "member" )"2" (case-replace "y!1(x!2)" )"1" (case-replace "x!1(x!2)" )"1" (inst + "0" ) nil nil )"2" (assert )"2" (inst + "1" ) (("2" (assert ) nil nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"set" sets nil )"set" sets nil )"set" sets nil )"[T, T -> boolean]" equalities nil )IF const-decl "[boolean, T, T -> T]" if_def nil )nil sequences nil )set type-eq-decl nil sets nil )nil outer_measure_props 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 outer_measure_props nil )"bool" sets nil )nil real_types nil )nil extended_nnreal"extended_nnreal/" )"extended_nnreal" extended_nnreal"extended_nnreal/" )"bool" outer_measure_def nil )nil outer_measure_def nil )"outer_measure" outer_measure_props nil )"extended_nnreal" extended_nnreal"extended_nnreal/" )"bool" reals nil )"[bool, bool -> bool]" booleans nil )"real" sigma "reals/" )"(strict_total_order?[real])" real_props nil )nil sigma_nat "reals/" )"sequence[real]" series "series/" )nil series_lems "series/" )"(strict_total_order?[real])" real_props nil )nil series_lems "series/" )"nnreal" nil )"finite_set" finite_sets nil )"finite_set[T]" countable_props"sets_aux/" )"finite_set[T]" bounded_nats"orders/" )nil outer_measure_props nil )"T3" function_props nil )"set[T]" indexed_sets nil ))nil 3396788683"" (skosimp*)"" (expand "outer_measurable?" )"" (split)"1" (skosimp*)"1" (inst - "y!1" ) (("1" (grind) nil nil )) nil )) nil )"2" (skosimp*)"2" (inst - "y!1" )"2" (lemma "pairwise_subadditive" ("x" "x!1" "y" "y!1" ))"2" "x_le_antisymmetric" "x" "m(y!1)" "y" "x_add(m(intersection(y!1, x!1)), ")) "2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" outer_measure_props nil )nil outer_measure_props nil )nil extended_nnreal"extended_nnreal/" )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil real_types nil )nil extended_nnreal"extended_nnreal/" )"bool" outer_measure_def nil )nil outer_measure_def nil )"outer_measure" outer_measure_props nil )"set" sets nil )"set" sets nil )"(total_order?[real])" nil )"nnreal" nil )"extended_nnreal" extended_nnreal"extended_nnreal/" )"bool" extended_nnreal "extended_nnreal/" )"bool" extended_nnreal "extended_nnreal/" )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil outer_measure_props nil ))nil 3396763601"" (skosimp)"" (typepred "x!1" )"" (rewrite "outer_measurable_def" )"" (skosimp)"" (expand "outer_negligible?" )"" "m_outer_increasing" "x" "intersection(y!1, x!1)" "y" "x!1" ))"" (split -1)"1" (expand "x_le" -1)"1" (replace -2)"1" (assert )"1" (flatten)"1" (expand "x_add" )"1" (replace -1)"1" (assert )"1" "m(intersection(y!1, x!1))`2 = 0" )"1" "1" assert )"1" "m_outer_increasing" "x" "intersection(y!1, complement(x!1))" "y" "y!1" ))"1" "1" expand "x_le" )"1" "m(y!1)`1" )"1" "1" assert )"1" replace -2)"1" nil nil ))nil ))nil ))nil )"2" replace 1)"2" (propax) nil nil ))nil ))nil ))nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "m(intersection(y!1, x!1))`2" )"2" "DRL" "m(intersection(y!1, x!1))`2" )"2" "reals_totally_ordered" )"2" expand "strict_total_order?" )"2" expand "trichotomous?" )"2" expand "strict_order?" )"2" "2" expand ">=" )"2" expand "<=" )"2" replace 1)"2" "1" expand "transitive?" )"1" "DRL" "0" "DRL" )"1" assert )"1" replace "1" nil nil ))nil ))nil ))nil ))nil )"2" assert )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" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil outer_measure_propsnil )"bool" outer_measure_props nil )set type-eq-decl nil sets nil )nil outer_measure_props nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"set" sets nil )nil outer_measure_props nil )"bool" extended_nnreal "extended_nnreal/" )"(total_order?[real])" nil )"extended_nnreal" extended_nnreal"extended_nnreal/" )"nnreal" nil )"(strict_total_order?[real])" real_props nil )"bool" orders nil )"bool" orders nil )"bool" relations nil )"bool" reals nil )"bool" orders nil )nil reals nil )"set" sets nil )"bool" sets nil )"bool" sets nil )"(partial_order?[set[T]])" nil )"outer_measure" outer_measure_props nil )nil outer_measure_def nil )"bool" outer_measure_def nil )nil extended_nnreal"extended_nnreal/" )nil real_types nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )"[T, T -> boolean]" equalities nil )nil numbers nil )nil outer_measure_props nil ))nil ))nil 3396585602"" (skosimp)"" (typepred "a!1" )"" (expand "outer_measurable?" )"" (skosimp*)"" (inst - "y!1" )"" (rewrite "complement_complement" )"" (lemma "x_add_commutative" )"" (expand "commutative?" )"" "m(intersection(y!1, a!1))" "m(intersection(y!1, complement(a!1)))" )"" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil outer_measure_propsnil )"bool" outer_measure_props nil )set type-eq-decl nil sets nil )nil outer_measure_props nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil sets_lemmas nil )"bool" operator_defs nil )"set" sets nil )"set" sets nil )"outer_measure" outer_measure_props nil )nil outer_measure_def nil )"bool" outer_measure_def nil )nil extended_nnreal"extended_nnreal/" )nil real_types nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil extended_nnreal"extended_nnreal/" ))nil ))nil 3408180473"" (judgement-tcc)"1" (rewrite "complement_emptyset" )"1" (rewrite "intersection_empty" )"1" (rewrite "intersection_full" )"1" (rewrite "m_outer_empty" )"1" (expand "x_add" ) (("1" (propax) nil nil )) nil )) nil ))nil ))nil ))nil )"2" (rewrite "complement_emptyset" )"2" (rewrite "intersection_full" )"2" (rewrite "intersection_empty" )"2" (rewrite "m_outer_empty" )"2" (expand "x_add" ) (("2" (propax) nil nil )) nil )) nil ))nil ))nil ))nil )"3" (rewrite "intersection_empty" )"3" (rewrite "m_outer_empty" )"3" (rewrite "complement_emptyset" )"3" (rewrite "intersection_full" )"3" (expand "x_add" ) (("3" (propax) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )nil outer_measure_props nil )nil sets_lemmas nil )nil sets_lemmas nil )"extended_nnreal" extended_nnreal"extended_nnreal/" )nil outer_measure_props nil )nil sets_lemmas nil )nil booleans nil )nil booleans nil )set type-eq-decl nil sets nil )"finite_set[T]" "orders/" )"finite_set[T]" bounded_nats"orders/" )"finite_set[T]" countable_props"sets_aux/" )"finite_set" finite_sets nil )"bool" extended_nnreal "extended_nnreal/" )"bool" outer_measure_props nil ))nil ))nil 3396585602"" (lemma "outer_measurable_emptyset" )"" (lemma "outer_measurable_complement" ("a" "emptyset[T]" ))"" (rewrite "complement_emptyset" ) nil nil )) nil ))nil )"set" sets nil )nil outer_measure_propsnil )"bool" outer_measure_props nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil outer_measure_props nil )nil outer_measure_propsnil )"outer_measurable" nil )"finite_set[T]" bounded_nats"orders/" )"finite_set[T]" countable_props"sets_aux/" )"finite_set" finite_sets nil )nil sets_lemmas nil )nil outer_measure_propsnil ))nil ))nil 3396585602"" (skosimp)"" (typepred "b!1" )"" (typepred "a!1" )"" (expand "outer_measurable?" )"" (skosimp)"" (inst-cp - "intersection(y!1,union(a!1,b!1))" )"" "intersection(intersection(y!1, union(a!1, b!1)), a!1)=intersection(y!1,a!1)" )"1" "intersection(intersection(y!1, union(a!1, b!1)), ") "1" (hide -1 -2)"1" (inst - "y!1" )"1" "intersection(y!1,complement(a!1))" )"1" (rewrite "intersection_associative" )"1" (rewrite "intersection_associative" )"1" (rewrite "demorgan1" -3 :dir rl)"1" "intersection_commutative" "a" "b!1" "b" "complement(a!1)" ))"1" replace -1)"1" "1" expand "x_add" )"1" expand "x_eq" )"1" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (apply-extensionality :hide? t)"2" (grind) nil nil )) nil ))nil ))nil )"2" (hide-all-but 1)"2" (apply-extensionality :hide? t)"2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil outer_measure_propsnil )"bool" outer_measure_props nil )set type-eq-decl nil sets nil )nil outer_measure_props nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"set" sets nil )"set" sets nil )"set" sets nil )"outer_measurable" outer_measure_props nil )nil sets_lemmas nil )nil sets_lemmas nil )"extended_nnreal" extended_nnreal"extended_nnreal/" )"nnreal" nil )"bool" extended_nnreal "extended_nnreal/" )nil sets_lemmas nil )"bool" sets nil )"[T, T -> boolean]" equalities nil ))nil ))nil 3396585602"" (skosimp)"" (typepred "b!1" )"" (typepred "a!1" )"" (lemma "outer_measurable_complement" ("a" "b!1" ))"" (lemma "outer_measurable_complement" ("a" "a!1" ))"" "outer_measurable_union" "a" "complement[T](a!1)" "b" "complement[T](b!1)" ))"" "outer_measurable_complement" "a" "union[T](complement[T](a!1), complement[T](b!1))" ))"" (rewrite "demorgan1" )"" (rewrite "complement_complement" )"" (rewrite "complement_complement" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil outer_measure_propsnil )"bool" outer_measure_props nil )set type-eq-decl nil sets nil )nil outer_measure_props nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil outer_measure_propsnil )"outer_measurable" outer_measure_props nil )nil outer_measure_props nil )"set" sets nil )nil sets_lemmas nil )nil sets_lemmas nil )"set" sets nil )"outer_measurable" nil ))nil ))nil 3396585602"" (skosimp)"" (rewrite "difference_intersection" )"" (typepred "b!1" )"" (typepred "a!1" )"" (lemma "outer_measurable_complement" ("a" "b!1" ))"" "outer_measurable_intersection" "a" "a!1" "b" "complement[T](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" outer_measure_props nil )nil outer_measure_propsnil )nil outer_measure_props nil )"outer_measurable" outer_measure_props nil )"outer_measurable" outer_measure_props nil )nil nil )"set" sets nil )nil outer_measure_propsnil )NOT const-decl "[bool -> bool]" booleans nil ))nil ))nil 3396587624"" (skosimp)"" (typepred "a!1" )"" (expand "outer_measurable?" )"" (inst - "intersection(x!1,union(a!1,b!1))" )"" "intersection(intersection(x!1, union(a!1, b!1)), a!1)=intersection(x!1,a!1)" )"1" "intersection(intersection(x!1, union(a!1, b!1)), ") "1" (hide -1 -2)"1" "intersection(x!1, intersection(b!1, complement(a!1)))=intersection(x!1, b!1)" )"1" (hide-all-but (-2 1))"1" (apply-extensionality :hide? t)"1" (expand "disjoint?" )"1" (expand "empty?" )"1" (inst - "x!2" ) (("1" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (apply-extensionality :hide? t)"2" (grind) nil nil )) nil ))nil ))nil )"2" (hide-all-but 1)"2" (apply-extensionality :hide? t)"2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )nil outer_measure_propsnil )"bool" outer_measure_props nil )set type-eq-decl nil sets nil )nil outer_measure_props nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"outer_measurable" nil )"set" sets nil )"set" sets nil )"set" sets nil )"outer_measurable" outer_measure_props nil )"outer_measurable" outer_measure_props nil )"bool" sets nil )"bool" sets nil )"bool" sets nil )"[T, T -> boolean]" equalities nil ))nil 3396588211"" case "forall X: increasing?(X)=>outer_measurable?(IUnion[nat, T](X))" )"1" (skosimp)"1" "E" "lambda (n:nat): IUnion(lambda i: if i<=n then X!1(i) else emptyset[T] endif)" )"1" (inst - "E" )"1" (split -2)"1" (hide -2)"1" "IUnion[nat, T](E)=IUnion[nat, T](X!1)" )"1" (hide -1 2)"1" (apply-extensionality :hide? t)"1" (expand "E" )"1" (case-replace "IUnion[nat, T](X!1)(x!1)" )"1" (expand "IUnion" )"1" (expand "emptyset" )"1" (skosimp)"1" "i!1" )"1" "i!1" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (expand "IUnion" )"2" (skosimp*)"2" expand "emptyset" )"2" "2" (inst + "i!2" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (expand "increasing?" )"2" (expand "E" )"2" (expand "IUnion" )"2" (expand "emptyset" )"2" (skolem + ("i" "j" ))"2" (flatten)"2" (expand "subset?" )"2" (expand "member" )"2" "2" "2" "i!1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (case "E(0)=X!1(0)" )"1" case "forall (n:nat): E(n+1)=union(E(n),X!1(n+1))" )"1" (induct "x1" )"1" (assert ) nil nil )"2" (skosimp)"2" (inst - "j!1" )"2" (assert )"2" "outer_measurable_union" "a" "E(j!1)" "b" "X!1(1 + j!1)" ))"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skosimp)"2" (expand "E" )"2" (hide -1)"2" (expand "IUnion" )"2" (expand "emptyset" )"2" (expand "union" )"2" expand "member" )"2" "2" "(EXISTS (i_1: nat): IF i_1 <= 1 + n!1 THEN X!1(i_1)(x!1) ELSE FALSE ENDIF)") "1" "1" "1" expand "<=" -1)"1" "1" "i!1" )"1" (assert ) nil nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" replace 1 2)"2" assert )"2" "1" "1" "1" "i!1" )"1" assert )nil nil ))nil ))nil ))nil )"2" "1+n!1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (expand "E" )"2" (expand "IUnion" )"2" (expand "emptyset" )"2" (apply-extensionality :hide? t)"2" (case-replace "X!1(0)(x!1)" )"1" (inst + "0" ) (("1" (assert ) nil nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" case "forall X: disjoint?(X)=> outer_measurable?(IUnion[nat, T](X))" )"1" (skosimp)"1" "E" "lambda i: if i=0 then X!1(0) else difference(X!1(i),X!1(i-1)) endif" )"1" (inst - "E" )"1" (hide -1)"1" (split)"1" "IUnion[nat, T](E)=IUnion[nat, T](X!1)" )"1" (hide -1 2)"1" (apply-extensionality :hide? t)"1" (case-replace "IUnion[nat, T](X!1)(x!1)" )"1" (expand "IUnion" )"1" (expand "E" )"1" expand "difference" )"1" expand "member" )"1" "1" "i!1=0" )"1" (inst + "0" ) nil nil )"2" "II" "{n:nat| n <= i!1 & X!1(n)(x!1)}" )"2" "every_nonempty_set_has_least[nat]" )"2" "II" )"1" expand "has_least?" )"1" "1" "t!1" )"1" expand "least?" )"1" expand "restrict" )"1" "1" expand "lower_bound?" )"1" "t!1" )"1" "1" expand "II" )"1" "1" assert )"1" "t!1=0" )"1" case "NOT II(t!1-1)" )"1" expand "II" )"1" assert )nil nil ))nil )"2" expand "II" )"2" "t!1-1" )"1" assert )nil nil )"2" assert )"2" expand "II" )"2" nil nil ))nil ))nil ))nil ))nil )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "nonempty?" )"2" expand "empty?" )"2" "i!1" )"2" expand "member" )"2" expand "II" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (expand "E" )"2" expand "IUnion" )"2" "2" "i!1 = 0" )"1" (inst + "0" ) nil nil )"2" assert )"2" expand "difference" )"2" "2" expand "member" )"2" "i!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (expand "disjoint?" )"2" case "forall (i,j:nat): disjoint?(E(i),E(i+1+j))" )"1" (skosimp)"1" "trich_lt" ("x" "i!1" "y" "j!1" ))"1" (split -1)"1" "i!1" "j!1-i!1-1" )"1" (assert ) nil nil )"2" (assert ) nil nil ))nil )"2" (propax) nil nil )"3" "j!1" "i!1-j!1-1" )"1" "1" expand "disjoint?" )"1" rewrite "intersection_commutative" )nil nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skolem + ("i" "_" ))"2" (induct "j" )"1" expand "disjoint?" )"1" expand "increasing?" )"1" expand "E" )"1" "i=0" )"1" "0" "1" )"1" assert )"1" expand "subset?" )"1" expand "intersection" )"1" expand "difference" )"1" expand "empty?" )"1" expand "member" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" expand "subset?" )"2" expand "difference" )"2" expand "intersection" )"2" expand "empty?" )"2" expand "member" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "increasing?" )"2" expand "disjoint?" )"2" expand "subset?" )"2" expand "intersection" )"2" expand "E" )"2" expand "difference" )"2" expand "empty?" )"2" expand "member" )"2" "2" "i=0" )"1" "0" "1+j!1" )"1" assert )"1" "x!1" )"1" assert )nil nil ))nil ))nil ))nil )"2" assert )"2" "2" "i" "1+i+j!1" )"2" assert )"2" "x!1" )"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 )"2" (skosimp) (("2" (assert ) nil nil )) nil ))nil ))nil )"2" (hide 2)"2" (skosimp)"2" (expand "outer_measurable?" )"2" (skolem + ("a" ))"2" (typepred "m" )"2" (name "E" "IUnion[nat, T](X!1)" )"2" (replace -1)"2" "En" "lambda (n:nat): IUnion(lambda i: if i<=n then X!1(i) else emptyset[T] endif)" )"2" (case "increasing?(En) & IUnion(En) = E" )"1" (flatten)"1" (case "En(0)=X!1(0)" )"1" case "forall (n:nat): disjoint?(En(n),X!1(n+1)) & union(En(n),X!1(n+1))=En(n+1)" )"1" case "forall (n:nat): outer_measurable?(En(n))" )"1" case "forall (n:nat): x_eq(m(intersection(a,En(n))),x_sigma(0,n,lambda i: m(intersection(a,X!1(i)))))" )"1" case "forall (n:nat): subset?(intersection(a, En(n)),E)" )"1" case "forall (n:nat): x_le(m(intersection(a, complement(E))),m(intersection(a, complement(En(n)))))" )"1" case "forall (n:nat): x_le(x_add(m(intersection(a, En(n))),m(intersection(a, complement(E)))),m(a))" )"1" case "x_le(x_add(x_sum(lambda i: m(intersection(a,X!1(i)))), ") "1" expand "outer_measure?" )"1" "1" expand "om_countably_subadditive?" )"1" case "x_le( m(intersection(a,E)),x_sum(LAMBDA i: m(intersection(a, X!1(i)))))" )"1" "1" case "x_le(x_add(m(intersection(a,E)),m(intersection(a,complement(E)))), LAMBDA i: m(intersection(a, X!1(i)))),m(intersection(a,complement(E)))))") "1" "1" case "x_le(m(a),x_add(m(intersection(a, E)), m(intersection(a, complement(E)))))" )"1" "INT1" "x_add(m(intersection(a, E)), m(intersection(a, complement(E))))" )"1" "INT2" "x_add(x_sum(LAMBDA i: m(intersection(a, X!1(i)))), ") "1" "1" "x_le_preorder" )"1" expand "preorder?" )"1" "1" expand "transitive?" )"1" "INT1" "INT2" "m(a)" )"1" assert )"1" "x_le_antisymmetric" "x" "m(a)" "y" "INT1" ))"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "pairwise_subadditive" "y" "a" "x" "E" ))"2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "LHS" "m(intersection(a, E))" )"2" "RHS" "x_sum(LAMBDA i: m(intersection(a, X!1(i))))" )"2" "ADD" "m(intersection(a, complement(E)))" )"2" expand "x_add" )"2" expand "x_le" )"2" "RHS`1" )"1" "1" "1" assert )nil nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "LAMBDA i: intersection(a, X!1(i))" )"2" expand "o" "2" "RHS" "x_sum(LAMBDA i: m(intersection(a, X!1(i))))" )"2" "IUnion(LAMBDA i: intersection(a, X!1(i)))=intersection(a, E)" )"2" "2" "2" "2" expand "intersection" )"2" expand "member" )"2" "a(x!1)" )"1" "E(x!1)" )"1" replace "1" "1" expand "IUnion" )"1" "1" "i!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" replace "2" "2" expand "IUnion" )"2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" expand "IUnion" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "macE" "m(intersection(a, complement(E)))" )"2" expand "x_le" 1)"2" "2" assert )"2" expand "x_add" "2" expand "x_le" "2" "macE`1" )"1" expand "x_sum" )"1" "(FORALL (i_1: nat): m(intersection(a, X!1(i_1)))`1)" )"1" "series(LAMBDA (i_2: nat): lambda i: m(intersection(a, En(i)))`2") "1" "1" "1" assert )"1" case " FORALL (n: nat):m(intersection(a, En(n)))`1" )"1" case "FORALL (n: nat):m(intersection(a, En(n)))`2 + macE`2<=m(a)`2" )"1" "1" case "bounded_above?(LAMBDA i: m(intersection(a, En(i)))`2)" )"1" "increasing_bounded_convergence" "v1" "LAMBDA i: m(intersection(a, En(i)))`2" ))"1" "increasing?(LAMBDA i: m(intersection(a, En(i)))`2)" )"1" "convergence_sequences.convergent?(LAMBDA (i_1: nat): m(intersection(a, En(i_1)))`2)" )"1" rewrite "limit_def" "1" replace "1" "1" expand "sup" )"1" expand "Im" )"1" "lub({z:real | EXISTS (n: nat): z = m(intersection(a, En(n)))`2})" )"1" "LUB" "lub({z: real | ") "1" "1" expand "least_upper_bound?" )"1" "1" case "LUB>m(a)`2-macE`2" )"1" "1" "m(a)`2 - macE`2" )"1" assert )"1" expand "upper_bound?" )"1" "1" "s!1" )"1" "1" "n!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "1" expand "nonempty?" )"1" expand "empty?" )"1" expand "member" )"1" "m(intersection[T](a, En(0)))`2" )"1" "0" )nil nil ))nil ))nil ))nil ))nil )"2" expand "bounded_above?" )"2" "2" "a!1" )"2" expand "upper_bound?" )"2" "2" "s!1" )"2" "2" "n!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "convergence_sequences.convergent?" )"2" expand "sup" )"2" "lub(Im(LAMBDA i: m(intersection(a, En(i)))`2))" )nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "outer_measure?" )"2" "2" expand "om_increasing?" )"2" expand "increasing?" )"2" "2" "x!1" "y!1" )"2" assert )"2" "intersection(a, En(x!1))" "intersection(a, En(y!1))" )"2" "1" expand "x_le" "1" "y!1" )nil nil ))nil )"2" "2" expand "intersection" )"2" expand "subset?" )"2" expand "member" )"2" "2" "x!2" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil )"2" "2" expand "bounded_above?" )"2" "m(a)`2" )"2" "2" "x!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "n!1" )"2" "n!1" )"2" replace "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "n!1" )"2" replace "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "series" )"2" "x!1" )"2" "x!1" )"2" expand "x_eq" "2" "2" expand "outer_measure?" )"2" "2" expand "om_increasing?" )"2" "intersection(a, En(x!1))" "a" )"2" "1" expand "x_le" "1" "1" replace "1" assert )"1" replace "1" expand "x_sigma" )"1" "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "subset?" )"2" expand "intersection" )"2" expand "member" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "n!1" ))"2" "0" )"2" expand "outer_measure?" )"2" "2" expand "om_increasing?" )"2" "intersection(a, X!1(n!1))" "a" )"2" "1" expand "x_le" )"1" nil nil ))nil )"2" "2" expand "intersection" )"2" expand "subset?" )"2" expand "member" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "0" )"2" replace "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "n!1" )"2" "n!1" )"2" "n!1" )"2" "2" expand "outer_measurable?" )"2" "a" )"2" "maEn" "m(intersection(a, En(n!1)))" )"2" "macE" "m(intersection(a, complement(E)))" )"2" "macEn" "m(intersection(a, complement(En(n!1))))" )"2" "2" expand "x_le" )"2" expand "x_eq" )"2" expand "x_add" )"2" "maEn`1" )"1" "1" "macE`1" )"1" assert )"1" "macEn`1" )"1" assert )nil nil )"2" assert )nil nil ))nil ))nil )"2" assert )nil nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "outer_measure?" )"2" "2" expand "om_increasing?" )"2" "n!1" )"2" "intersection(a, complement(E))" "intersection(a, complement(En(n!1)))" )"2" "1" nil nil )"2" "2" expand "complement" )"2" expand "intersection" )"2" expand "subset?" )"2" expand "member" )"2" "2" "x!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "intersection" )"2" expand "subset?" )"2" expand "member" )"2" expand "En" )"2" expand "IUnion" )"2" expand "emptyset" )"2" "2" "2" expand "E" )"2" expand "IUnion" )"2" "i!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "n" )"1" replace -3)"1" expand "x_sigma" )"1" expand "x_eq" )"1" "m(intersection(a, X!1(0)))`1" )"1" "FORALL (i_1: nat): i_1 <= 0 => m(intersection(a, X!1(i_1)))`1" )"1" expand "sigma" )"1" expand "sigma" )"1" nil nil ))nil ))nil )"2" "2" "2" "i!1" )"2" expand ">=" )"2" expand "<=" )"2" replace "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace 1)"2" "2" "FORALL (i_1: nat): i_1 <= 0 => m(intersection(a, X!1(i_1)))`1" )"1" "0" )"1" assert )nil nil ))nil )"2" replace 1 3)"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "j!1" )"2" "j!1" )"2" "2" "outer_measurable_disjoint_union" "x" "a" "a" "En(j!1)" "b" "X!1(j!1 + 1)" ))"1" assert )"1" replace -5 -1)"1" "1" "X1" "m(intersection(a, En(1 + j!1)))" )"1" "X2" "m(intersection(a, En(j!1)))" )"1" expand "x_add" )"1" expand "x_eq" )"1" expand "x_sigma" )"1" expand "sigma" "1" "X1`1" )"1" "1" "1" replace "1" replace "1" "1" "1" "i!1" )"1" assert )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace "2" "2" replace "2" replace "2" replace "2" "FORALL (i_1: nat): ") "1" assert )nil nil )"2" "2" "i!1" )"2" "i!1" )"2" assert )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace "2" "2" assert )"2" "X2`1" )"1" "1" "1+j!1" )"1" assert )nil nil ))nil ))nil )"2" replace "2" "2" "2" "i!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "n" )"1" replace -2)"1" (assert ) nil nil ))nil )"2" "2" "j!1" )"2" "2" "outer_measurable_union" "a" "En(j!1)" "b" "X!1(j!1 + 1)" ))"1" (assert ) nil nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "n" )"1" replace -1)"1" expand "disjoint?" )"1" expand "disjoint?" )"1" "0" "1" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" replace -1)"2" "2" expand "En" )"2" "2" expand "union" )"2" expand "IUnion" )"2" expand "emptyset" )"2" expand "member" )"2" "X!1(0)(x!1)" )"1" "0" )"1" assert )nil nil ))nil )"2" "X!1(1)(x!1)" )"1" "1" )"1" assert )nil nil ))nil )"2" assert )"2" "2" "2" "i!1=0" )"2" "i!1=1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "1" replace -2 1 rl)"1" "1" expand "union" )"1" expand "disjoint?" )"1" expand "disjoint?" )"1" expand "intersection" )"1" expand "empty?" )"1" expand "member" )"1" "1" "1" "x!1" )"1" assert )"1" expand "En" "1" expand "IUnion" )"1" expand "emptyset" )"1" "1" "1" "i!1" "2+j!1" )"1" assert )"1" "x!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "1+j!1" "2+j!1" )"2" assert )"2" "x!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "En" )"2" expand "union" )"2" "2" expand "member" )"2" expand "IUnion" )"2" "(EXISTS (i_1: nat): IF i_1 <= 2 + j!1 THEN X!1(i_1)(x!1) ELSE emptyset[T](x!1) ENDIF)") "1" "1" "1" expand "<=" "1" "1" "i!1" )"1" assert )nil nil ))nil )"2" assert )nil nil ))nil ))nil )"2" expand "emptyset" )"2" nil nil ))nil ))nil ))nil )"2" replace 1 2)"2" assert )"2" "1" "1" "1" "i!1" )"1" assert )nil nil ))nil )"2" expand "emptyset" )"2" nil nil ))nil ))nil ))nil )"2" "2+j!1" )"2" expand "emptyset" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "En" )"2" "2" expand "IUnion" )"2" expand "emptyset" )"2" "X!1(0)(x!1)" )"1" "0" )"1" (assert ) nil nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -1 -3 2)"2" (split)"1" expand "increasing?" )"1" "i" "j" ))"1" "1" expand "subset?" )"1" expand "En" )"1" expand "IUnion" )"1" expand "emptyset" )"1" expand "member" )"1" "1" "1" "i!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "E" )"2" "2" expand "En" )"2" expand "IUnion" )"2" expand "emptyset" )"2" "EXISTS (i: nat): X!1(i)(x!1)" )"1" "1" "i!1" )"1" "i!1" )"1" assert )nil nil ))nil ))nil ))nil )"2" replace 1 2)"2" assert )"2" "2" "2" "i!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 real_types nil )nil extended_nnreal"extended_nnreal/" )"bool" outer_measure_def nil )nil outer_measure_def nil )"outer_measure" outer_measure_props nil )"outer_measurable" nil )"real" sigma "reals/" )nil nil )"extended_nnreal" extended_nnreal"extended_nnreal/" )"sequence[real]" series "series/" )nil "analysis/" )"bool" outer_measure_def nil )"bool" convergence_sequences "analysis/" )"bool" bounded_real_defs nil )"bool" bounded_real_defs nil )"{x | least_upper_bound?(x, SA)}" bounded_real_defsnil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"bool" bounded_real_defs nil )"bool" reals nil )"real" reals nil )"setof[real]" real_fun_props "reals/" )nil convergence_sequences "analysis/" )"real" real_fun_supinf "analysis/" )"(nonempty?[real])" "extended_nnreal/" )nil defined_types nil )"bool" real_fun_preds "reals/" )"bool" real_fun_preds "reals/" )"nnreal" sigma_nat "reals/" )"bool" outer_measure_def nil )"T3" function_props nil )"nnreal" nil )nil outer_measure_props nil )"bool" orders nil )"bool" relations nil )nil extended_nnreal"extended_nnreal/" )nil extended_nnreal "extended_nnreal/" )"extended_nnreal" extended_nnreal"extended_nnreal/" )"set" sets nil )"bool" extended_nnreal "extended_nnreal/" )"[nat -> set[T]]" outer_measure_props nil )"set[T]" outer_measure_props nil )"extended_nnreal" extended_nnreal"extended_nnreal/" )"bool" extended_nnreal "extended_nnreal/" )"[nat -> outer_measurable]" nil )nil bounded_nats"orders/" )"bool" sets nil )"bool" minmax_orders "orders/" )"bool" bounded_orders "orders/" )"nat" outer_measure_props nil )"(total_order?[real])" nil )"bool" minmax_orders "orders/" )"[nat -> boolean]" outer_measure_props nil )"bool" sets nil )AND const-decl "[bool, bool -> bool]" booleans nil )"odd_int" integers nil )"set" sets nil )"even_int" integersnil )"int" integers nil )"nat" outer_measure_props nil )"nat" outer_measure_props nil )nil sets_lemmas nil )"outer_measurable" outer_measure_props nil )nil real_props nil )"bool" sets nil )NOT const-decl "[bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )"set" sets nil )"outer_measurable" outer_measure_props nil )"bool" indexed_sets_aux "sets_aux/" )"[nat -> set[T]]" outer_measure_props nil )"bool" sets nil )"(total_order?[real])" nil )"bool" booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )nil defined_types nil )nil naturalnumbers nil )"posint" nil )nil outer_measure_props nil )"set" sets nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"posint" nil )"set" sets nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"[T, T -> boolean]" equalities nil )"finite_set" finite_sets nil )"(total_order?[S])" nil )"(dichotomous?[S])" nil )"(partial_order?[S])" nil )"(preorder?[S])" nil )"(transitive?[S])" nil )"(antisymmetric?[S])" nil )"(reflexive?[S])" nil )"(partial_order?[set[T]])" nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )nil outer_measure_props nil )set type-eq-decl nil sets nil )"bool" outer_measure_props nil )nil outer_measure_propsnil )nil sequences nil )"[bool, bool -> bool]" booleans nil )"R" restrict nil )"bool" reals nil )"bool" sets nil )"bool" fun_preds_partial "structures/" )"set[T]" indexed_sets nil ))nil ))nil 3396588211"" (skosimp)"" (lemma "outer_measurable_IUnion" ("X" "IComplement(X!1)" ))"1" (rewrite "IDemorgan2" * :dir rl)"1" "outer_measurable_complement" "a" "complement(IIntersection(X!1))" ))"1" (rewrite "complement_complement" ) nil nil )"2" (propax) nil nil ))nil ))nil )"2" (skolem + ("n!1" ))"2" (hide 2)"2" (typepred "X!1(n!1)" )"2" (expand "IComplement" ) (("2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"set[T]" indexed_sets_aux "sets_aux/" )nil sequences nil )nil outer_measure_propsnil )"bool" outer_measure_props nil )set type-eq-decl nil sets nil )nil outer_measure_props 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 outer_measure_props nil )"set[T]" indexed_sets nil )"set" sets nil )nil outer_measure_propsnil )nil sets_lemmas nil )nil indexed_sets_aux "sets_aux/" )"outer_measurable" outer_measure_props nil )NOT const-decl "[bool -> bool]" booleans nil ))nil ))nil 3397465978"" (skosimp)"" (expand "is_countable" )"" (skosimp)"" (typepred "f!1" )"" (expand "injective?" )"" "XX" "lambda (n:nat): if (exists (x:(S!1)): f!1(x) = n) then choose({x:(S!1) | f!1(x)=n}) else emptyset[T] endif" )"1" (case "IUnion(XX)=Union(S!1)" )"1" (lemma "outer_measurable_IUnion" ("X" "XX" ))"1" (replace -2) (("1" (propax) nil nil )) nil )"2" (expand "every" )"2" (hide-all-but (-3 -4 1))"2" (skolem + ("n!1" ))"2" (expand "XX" )"2" "EXISTS (x: (S!1)): f!1(x) = n!1" )"1" (skosimp)"1" "x!1" )"1" "choose_member" "a" "{x_1: (S!1) | f!1(x_1) = n!1}" ))"1" "1" expand "member" )"1" "choose({x_1: (S!1) | f!1(x_1) = n!1})" "x!1" )"1" (assert ) nil nil )"2" expand "nonempty?" )"2" expand "empty?" )"2" "x!1" )"2" expand "member" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "empty?" )"2" "x!1" )"2" expand "member" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (replace 1 2)"2" rewrite "outer_measurable_emptyset" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -1 2 -3)"2" (apply-extensionality :hide? t)"2" (expand "Union" )"2" (case-replace "EXISTS (a: (S!1)): a(x!1)" )"1" (skosimp)"1" (typepred "a!1" )"1" (expand "XX" )"1" expand "IUnion" )"1" expand "emptyset" )"1" "f!1(a!1)" )"1" "EXISTS (x: (S!1)): f!1(x) = f!1(a!1)" )"1" "choose_member" "a" "{x_1: (S!1) | f!1(x_1) = f!1(a!1)}" ))"1" "1" expand "member" )"1" "choose({x_1: (S!1) | f!1(x_1) = f!1(a!1)})" "a!1" )"1" replace -1)"1" replace -5 1)"1" nil nil ))nil ))nil )"2" expand "nonempty?" )"2" expand "empty?" )"2" expand "member" )"2" "a!1" )nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "empty?" )"2" expand "member" )"2" "a!1" )nil nil ))nil ))nil ))nil ))nil )"2" (inst + "a!1" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (replace 1 2)"2" (assert )"2" (expand "XX" )"2" expand "IUnion" )"2" expand "emptyset" )"2" "2" "2" "2" "choose({x: (S!1) | f!1(x) = i!1})" )"2" expand "nonempty?" )"2" expand "empty?" )"2" expand "member" )"2" "x!2" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp)"2" (skosimp)"2" (expand "nonempty?" )"2" (expand "empty?" )"2" (inst - "x!1" )"2" (assert )"2" (expand "member" )"2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" 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 sets nil )nil defined_types nil )nil outer_measure_props nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"set" sets nil )"(p)" sets nil )"bool" sets nil )set type-eq-decl nil sets nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"[T, T -> boolean]" equalities nil )"[bool, bool -> bool]" booleans nil )"nat" outer_measure_props nil )"(S!1)" outer_measure_props nil )"(surjective?[setofsets[T], set[T]])" sets_lemmas nil )nil outer_measure_props nil )"bool" outer_measure_props nil )nil outer_measure_propsnil )nil sequences nil )"[nat -> setof[T]]" outer_measure_props nil )nil outer_measure_propsnil )nil sets_lemmas nil )"bool" sets nil )"bool" sets nil )"nat" outer_measure_props nil )"(injective?[(S!1), nat])" nil )"setofsets[T]" outer_measure_props nil )"bool" sets nil )"set" sets nil )"set[T]" indexed_sets nil ))nil 3397965002"" (skosimp)"" (lemma "outer_measurable_Union" ("S" "Complement(S!1)" ))"" (split)"1" "outer_measurable_complement" "a" "Union(Complement(S!1))" ))"1" (rewrite "Demorgan1" )"1" (rewrite "Complement_Complement" ) nil nil )) nil )"2" (propax) nil nil ))nil )"2" (hide -2 2)"2" (lemma "Complement_bijective[T]" )"2" (expand "bijective?" )"2" (flatten)"2" (expand "is_countable" )"2" (skosimp)"2" (typepred "f!1" )"2" (expand "injective?" )"2" "lambda (x:(Complement(S!1))): f!1(complement(x))" )"1" (expand "injective?" )"1" (skosimp)"1" "1" "x2!1" )"1" "x1!1" )"1" "1" expand "Complement" )"1" "1" "b!1" "b!2" )"1" replace -1)"1" replace -2)"1" rewrite "complement_complement" )"1" rewrite "complement_complement" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp)"2" (typepred "x!1" )"2" expand "Complement" )"2" "2" "b!1" )"2" replace -2)"2" rewrite "complement_complement" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide -1 2)"3" (expand "Complement" )"3" (expand "every" )"3" (skosimp)"3" (typepred "x!1" )"3" (skosimp)"3" (replace -1)"3" (inst - "b!1" )"3" "outer_measurable_complement" "a" "b!1" ))"1" (propax) nil nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"setofsets[T]" sets_lemmas nil )nil sets nil )nil defined_types nil )nil booleans nil )nil booleans nil )nil outer_measure_props nil )nil outer_measure_props nil )"bool" sets nil )"[T, T -> boolean]" equalities nil )"bool" functions nil )"bool" 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 )NOT const-decl "[bool -> bool]" booleans nil )"set" sets nil )"setofsets[T]" outer_measure_props nil )"(injective?[(S!1), nat])" nil )nil sets_lemmas nil )nil sets_lemmas nil )"set" sets nil )nil outer_measure_propsnil )"bool" outer_measure_props nil )set type-eq-decl nil sets nil )nil outer_measure_propsnil )"(surjective?[setofsets[T], set[T]])" sets_lemmas nil )"(bijective?[setofsets[T], setofsets[T]])" sets_lemmas nil )nil sets_lemmas nil )"(surjective?[setofsets[T], set[T]])" sets_lemmas nil )nil sets_lemmas nil ))nil 3397964035"" (skosimp)"" "x_le_antisymmetric" "x" "m(intersection(x!1, IUnion(X!1)))" "y" "x_sum(LAMBDA i: m(intersection(x!1, X!1(i))))" ))"" (assert )"" (hide 2)"" (split)"1" (typepred "m" )"1" (expand "outer_measure?" )"1" (flatten)"1" (expand "om_countably_subadditive?" )"1" "LAMBDA i: intersection(x!1, X!1(i))" )"1" (expand "o" )"1" "IUnion(LAMBDA i: intersection(x!1, X!1(i)))=intersection(x!1, IUnion(X!1))" )"1" (hide -3 2)"1" (apply-extensionality :hide? t)"1" expand "intersection" )"1" expand "IUnion" )"1" expand "member" )"1" "x!1(x!2)" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "x_le" )"2" (flatten)"2" (expand "x_sum" )"2" "FORALL i: m(intersection(x!1, X!1(i)))`1" )"1" (lift-if)"1" (assert )"1" "En" "lambda (n:nat): IUnion(LAMBDA i: IF i <= n THEN X!1(i)") "1" (hide -1)"1" case "En(0) =X!1(0) & forall (n:nat): En(n+1)=union(En(n), X!1(n+1))" )"1" "1" case "FORALL (n: nat): disjoint?(En(n),X!1(n+1))" )"1" case "FORALL (n: nat): outer_measurable?(En(n))" )"1" case "forall (n:nat): x_eq(m(intersection(x!1,En(n))),x_sigma(0,n,lambda i: m(intersection(x!1, X!1(i)))))" )"1" "series(LAMBDA (i_1: nat): lambda i: m(intersection(x!1, En(i)))`2") "1" "1" case "forall (n:nat): subset?(intersection(x!1, En(n)),intersection(x!1, IUnion(X!1)))" )"1" case "FORALL (n: nat):m(intersection(x!1, En(n)))`1" )"1" case "FORALL (n: nat):m(intersection(x!1, En(n)))`2<=m(intersection(x!1, IUnion(X!1)))`2" )"1" case "increasing?(LAMBDA i: m(intersection(x!1, En(i)))`2)" )"1" case "bounded_above?(LAMBDA i: m(intersection(x!1, En(i)))`2)" )"1" "increasing_bounded_convergence" "v1" "LAMBDA i: m(intersection(x!1, En(i)))`2" ))"1" assert )"1" "convergence_sequences.convergent?(LAMBDA i: m(intersection(x!1, En(i)))`2)" )"1" "1" rewrite "convergence_sequences.limit_def" "1" replace "1" "1" expand "sup" )"1" expand "Im" )"1" "lub({z:real | EXISTS (x: nat): z = m(intersection(x!1, En(x)))`2})" )"1" "LUB" "lub({z:real | EXISTS (x: nat): z = m(intersection(x!1, En(x)))`2})" )"1" expand "least_upper_bound?" )"1" "1" "m(intersection(x!1, IUnion(X!1)))`2" )"1" assert )"1" "1" expand "upper_bound?" "1" "1" "s!1" )"1" "1" "x!2" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "1" expand "nonempty?" )"1" expand "empty?" )"1" expand "member" )"1" "m(intersection[T](x!1, En(0)))`2" )"1" "0" )nil nil ))nil ))nil ))nil ))nil )"2" expand "bounded_above?" )"2" "2" expand "upper_bound?" )"2" "a!1" )"2" "2" "s!1" )"2" "2" "x!2" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "convergence_sequences.convergent?" )"2" expand "sup" )"2" "lub(Im(LAMBDA i: m(intersection(x!1, En(i)))`2))" )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "convergence_sequences.convergent?" )"2" expand "sup" )"2" "lub(Im(LAMBDA i: m(intersection(x!1, En(i)))`2))" )nil nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil )"2" "2" expand "bounded_above?" )"2" "m(intersection(x!1, IUnion(X!1)))`2" )nil nil ))nil ))nil ))nil )"2" "2" expand "increasing?" )"2" "i!1" "j!1" ))"2" "2" "2" "j!1" )"2" "m" )"2" expand "outer_measure?" )"2" "2" expand "om_increasing?" )"2" "intersection(x!1, En(i!1))" "intersection(x!1, En(j!1))" )"2" "1" expand "x_le" )"1" replace "1" nil nil ))nil ))nil )"2" "2" expand "En" )"2" expand "intersection" )"2" expand "subset?" )"2" expand "IUnion" )"2" expand "emptyset" )"2" expand "member" )"2" "2" "2" "i!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 )"2" "2" "2" "n!1" )"2" "n!1" )"2" "m" )"2" expand "outer_measure?" )"2" "2" expand "om_increasing?" )"2" "intersection(x!1, En(n!1))" "intersection(x!1, IUnion(X!1))" )"2" assert )"2" expand "x_le" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "n!1" )"2" "m" )"2" expand "outer_measure?" )"2" expand "om_increasing?" )"2" "2" "intersection(x!1, En(n!1))" "intersection(x!1, IUnion(X!1))" )"2" assert )"2" expand "x_le" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "En" )"2" expand "intersection" )"2" expand "subset?" )"2" expand "member" )"2" expand "IUnion" )"2" expand "emptyset" )"2" "2" "2" "i!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "series" )"2" "x!2" )"2" expand "x_eq" )"2" expand "x_sigma" )"2" "2" "FORALL (i_1: nat): ") "1" assert )nil nil )"2" "2" "i!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "n" )"1" replace -3)"1" expand "x_sigma" )"1" expand "sigma" )"1" expand "x_eq" )"1" "0" )"1" replace -5)"1" "1" assert )"1" "1" "1" "i!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "outer_measurable_disjoint_union" "x" "x!1" "a" "En(j!1)" "b" "X!1(j!1 + 1)" ))"2" "j!1" )"2" assert )"2" "intersection(x!1, union(En(j!1), X!1(1 + j!1)))=intersection(x!1, En(1 + j!1))" )"1" "1" expand "x_eq" )"1" expand "x_add" )"1" assert )"1" "1" expand "x_sigma" )"1" expand "sigma" "1" "m(intersection(x!1, En(1 + j!1)))`1" )"1" "1" replace "1" "1" "1" "i!1" )"1" assert )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" replace "2" "2" "FORALL (i_1: nat): ") "1" replace "1" replace "1" replace "1" replace "1" nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" "i!1" )"2" assert )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace "2" assert )"2" "FORALL (i_1: nat): ") "1" "FORALL (i_2: nat): ") "1" replace "1" "1+j!1" )"1" assert )nil nil ))nil ))nil )"2" "2" "i!1" )"2" assert )nil nil ))nil ))nil ))nil )"2" replace "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "intersection" )"2" expand "member" )"2" expand "union" )"2" expand "member" )"2" "j!1" )"2" replace "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "En" )"2" (propax) nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "disjoint?" )"2" expand "disjoint?" )"2" expand "intersection" )"2" expand "En" )"2" expand "empty?" )"2" expand "IUnion" )"2" expand "emptyset" )"2" expand "member" )"2" "2" "2" "2" "i!1" "1+n!1" )"2" assert )"2" "x!2" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "1" expand "En" )"1" "1" expand "IUnion" )"1" expand "emptyset" )"1" "X!1(0)(x!2)" )"1" "0" )"1" (assert ) nil nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "En" )"2" expand "union" )"2" expand "IUnion" )"2" expand "member" )"2" expand "emptyset" )"2" "2" "EXISTS (i_1: nat): IF i_1 <= 1 + n!1 THEN X!1(i_1)(x!2) ELSE FALSE ENDIF") "1" "1" "1" expand "<=" "1" "1" "i!1" )"1" assert )nil nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" replace 1 2)"2" assert )"2" "1" "1" "1" "i!1" )"1" assert )nil nil ))nil ))nil ))nil )"2" "1+n!1" )"2" 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" (skosimp)"2" (typepred "m" )"2" (expand "outer_measure?" )"2" (flatten)"2" expand "om_increasing?" )"2" "intersection(x!1, X!1(i!1))" "intersection(x!1, IUnion(X!1))" )"2" expand "x_le" )"2" assert )"2" "2" expand "subset?" )"2" expand "intersection" )"2" expand "member" )"2" "2" expand "IUnion" )"2" assert )"2" "i!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 )"extended_nnreal" extended_nnreal"extended_nnreal/" )nil sequences nil )nil outer_measure_propsnil )"bool" outer_measure_props nil )"set[T]" indexed_sets nil )nil naturalnumbers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"set" sets nil )"outer_measure" outer_measure_props nil )nil outer_measure_def nil )"bool" outer_measure_def nil )set type-eq-decl nil sets nil )nil outer_measure_props nil )nil extended_nnreal"extended_nnreal/" )nil real_types nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil booleans nil )nil booleans nil )nil extended_nnreal"extended_nnreal/" )"outer_measurable" nil )"bool" extended_nnreal "extended_nnreal/" )"finite_set" finite_sets nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"bool" reals nil )"set" sets nil )"outer_measurable" nil )"posint" nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"set" sets nil )"bool" sets nil )"bool" extended_nnreal "extended_nnreal/" )"extended_nnreal" extended_nnreal"extended_nnreal/" )"(strict_total_order?[real])" real_props nil )"nnreal" sigma_nat "reals/" )"[bool, bool -> bool]" booleans nil )"(partial_order?[set[T]])" nil )"bool" real_fun_preds "reals/" )nil "analysis/" )"bool" convergence_sequences "analysis/" )"real" real_fun_supinf "analysis/" )nil convergence_sequences "analysis/" )"(total_order?[real])" nil )"setof[real]" real_fun_props "reals/" )"bool" sets nil )"bool" bounded_real_defs nil )"{x | least_upper_bound?(x, SA)}" bounded_real_defsnil )"bool" bounded_real_defs nil )"bool" bounded_real_defs nil )"bool" sets nil )"(nonempty?[real])" "extended_nnreal/" )nil defined_types nil )"bool" real_fun_preds "reals/" )"bool" outer_measure_def nil )"[nat -> outer_measurable]" nil )"bool" sets nil )"sequence[real]" series "series/" )nil defined_types nil )nil naturalnumbers nil )nil sigma_nat "reals/" )"(total_order?[real])" nil )"real" sigma "reals/" )nil nil )"odd_int" integersnil )"extended_nnreal" extended_nnreal"extended_nnreal/" )"nnreal" nil )"int" integers nil )"posint" nil )"bool" indexed_sets_aux "sets_aux/" )"outer_measurable" outer_measure_props nil )OR const-decl "[bool, bool -> bool]" booleans nil )"bool" booleans nil )NOT const-decl "[bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )"bool" sets nil )"T3" function_props nil )"bool" outer_measure_defnil ))nil 3396790447"" (skosimp)"" "outer_measurable_disjoint_IUnion" "X" "X!1" "x" "fullset[T]" ))"" (assert )"" "intersection(fullset[T], IUnion(X!1))=IUnion(X!1)" )"1" (hide -1)"1" "(LAMBDA i: m(intersection(fullset[T], X!1(i)))) = m o X!1" )"1" (hide-all-but 1)"1" (apply-extensionality :hide? t)"1" (expand "o" )"1" (expand "fullset" )"1" (expand "intersection" )"1" (expand "member" )"1" "{x_1: T | X!1(x!1)(x_1)}=X!1(x!1)" )"1" (hide 2)"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (apply-extensionality :hide? t)"2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"set" sets nil )nil sequences nil )nil outer_measure_propsnil )"bool" outer_measure_props nil )set type-eq-decl nil sets nil )nil outer_measure_props 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 nil )"set[T]" indexed_sets nil )"set" sets nil )"[T, T -> boolean]" equalities nil )"outer_measurable" outer_measure_props nil )"outer_measurable" nil )nil real_types nil )nil extended_nnreal"extended_nnreal/" )"bool" outer_measure_def nil )nil outer_measure_def nil )"outer_measure" outer_measure_props nil )"T3" function_props nil )"bool" sets nil )"outer_measurable" nil ))nil 3397464661"" (expand "fullset" )"" (expand "extend" )"" (expand "sigma_algebra?" )"" (split)"1" (expand "subset_algebra_empty?" )"1" (expand "member" ) (("1" (propax) nil nil )) nil )) nil )"2" (expand "subset_algebra_complement?" )"2" (skosimp)"2" (expand "member" )"2" (typepred "x!1" )"2" (prop)"2" (assert )"2" "outer_measurable_complement" "a" "x!1" ))"2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (expand "sigma_algebra_union?" )"3" (skosimp*)"3" (expand "member" )"3" (prop)"3" (lemma "outer_measurable_Union" ("S" "X!1" ))"3" (assert )"3" (hide -1 2)"3" (expand "every" )"3" (skosimp)"3" (inst - "x!1" ) (("3" (prop) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"R" extend nil )"finite_set" finite_sets nil )"finite_set[T]" countable_props"sets_aux/" )"finite_set[T]" bounded_nats"orders/" )"outer_measurable" nil )"bool" sets nil )"bool" subset_algebra_def nil )"bool" booleans nil )IF const-decl "[boolean, T, T -> T]" if_def nil )nil defined_types nil )"bool" outer_measure_props nil )set type-eq-decl nil sets nil )nil outer_measure_props nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" booleans nil )nil booleans nil )nil booleans nil )nil outer_measure_propsnil )nil outer_measure_propsnil )"bool" subset_algebra_defnil )"(surjective?[setofsets[T], set[T]])" sets_lemmas nil )"bool" sets nil )nil outer_measure_props nil )nil sets nil )"bool" subset_algebra_def nil )"bool" subset_algebra_def nil )"set" sets nil ))nil 3453444636"" (lemma "outer_measurable_is_sigma_algebra" )"" (expand "fullset" )"" (expand "extend" )"" (expand "sigma_algebra?" )"" (flatten)"" (split)"1" (expand "subset_algebra_empty?" )"1" (expand "member" ) (("1" (propax) nil nil )) nil ))nil )"2" (expand "subset_algebra_complement?" )"2" (skosimp)"2" (expand "member" ) (("2" (propax) nil nil ))nil ))nil ))nil )"3" (expand "sigma_algebra_union?" )"3" (skosimp)"3" (expand "member" )"3" (inst -5 "X!1" )"3" (assert )"3" (skosimp)"3" (inst -2 "x!1" )"3" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"set" sets nil )"bool" subset_algebra_def nil )"finite_set" finite_sets nil )"finite_set[T]" countable_props"sets_aux/" )"finite_set[T]" bounded_nats"orders/" )"outer_measurable" nil )"bool" sets nil )"bool" subset_algebra_def nil )"outer_measurable" outer_measure_props nil )"bool" subset_algebra_defnil )nil sets nil )nil defined_types nil )nil booleans nil )nil booleans nil )nil outer_measure_props nil )"(surjective?[setofsets[T], set[T]])" sets_lemmas nil )"bool" subset_algebra_def nil )"R" extend nil )nil nil ))nil ))nil 3397469199"" (typepred "m" )"" (expand "restrict" )"" (expand "complete_measure?" )"" (expand "measure?" )"" (expand "outer_measure?" )"" (flatten)"" (split)"1" (expand "measure_empty?" )"1" (expand "om_empty?" ) (("1" (propax) nil nil ))nil ))nil )"2" (expand "measure_countably_additive?" )"2" (skosimp)"2" (typepred "X!1" )"2" "outer_measure_disjoint_IUnion" "X" "X!1" ))"1" (expand "disjoint_indexed_measurable?" )"1" (replace -2)"1" (hide-all-but (-1 1))"1" expand "x_eq" )"1" expand "o " )"1" "m(IUnion(X!1))`1" )"1" "1" (assert ) nil nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skolem + "n!1" )"2" (typepred "X!1(n!1)" )"2" (expand "induced_sigma_algebra" )"2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (expand "measure_complete?" )"3" (skosimp)"3" (expand "induced_sigma_algebra" )"3" (rewrite "outer_measurable_def" )"3" (skosimp)"3" (expand "om_increasing?" )"3" "m(intersection(y!1, x!1))=(TRUE,0)" )"1" expand "x_add" )"1" "intersection(y!1, complement(x!1))" "y!1" )"1" "1" expand "x_le" )"1" "m(y!1)`1" )"1" "1" assert )"1" replace -2)"1" (propax) nil nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil )"2" "2" "x!1" "a!1" )"2" replace -2)"2" "intersection(y!1, x!1)" "x!1" )"2" "1" expand "x_le" )"1" assert )"1" replace -2)"1" "1" assert )"1" replace -4)"1" "1" assert )"1" "1" "reals.<=" )"1" expand "total_order?" )"1" expand "partial_order?" )"1" expand "preorder?" )"1" "1" expand "transitive?" )"1" "m(intersection(y!1, x!1))`2" "m(x!1)`2" "0" )"1" assert )"1" replace "1" replace "1" assert )"1" "1" "m(intersection(y!1, x!1))`2" )"1" expand ">=" )"1" expand "antisymmetric?" )"1" "0" "m(intersection(y!1, x!1))`2" )"1" replace "1" replace "1" 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 )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"R" restrict nil )"bool" generalized_measure_def nil )"bool" generalized_measure_def nil )"bool" booleans nil )"set" sets nil )"[T, T -> boolean]" equalities nil )"set" sets nil )"bool" sets nil )"bool" sets nil )"bool" extended_nnreal "extended_nnreal/" )"(total_order?[real])" nil )"(partial_order?[set[T]])" nil )"extended_nnreal" extended_nnreal"extended_nnreal/" )"bool" orders nil )"bool" relations nil )"bool" relations nil )"bool" orders nil )"bool" reals nil )"bool" orders nil )nil defined_types nil )"bool" outer_measure_def nil )nil outer_measure_props nil )"bool" nil )nil nil )"bool" nil )"sigma_algebra[T]" nil )nil subset_algebra_def nil )"bool" subset_algebra_def nil )nil sets nil )nil defined_types nil )nil naturalnumbers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"T3" function_props nil )"set[T]" indexed_sets nil )"bool" extended_nnreal "extended_nnreal/" )nil sequences nil )nil outer_measure_propsnil )"bool" outer_measure_props nil )nil outer_measure_propsnil )"bool" generalized_measure_def nil )"bool" outer_measure_def nil )"bool" generalized_measure_def nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil outer_measure_props nil )set type-eq-decl nil sets nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil real_types nil )nil extended_nnreal"extended_nnreal/" )"bool" outer_measure_def nil )nil outer_measure_def nil )"outer_measure" outer_measure_props nil ))nil ))nil 3455093269 ("" (subtype-tcc) nil nil )"sigma_algebra[T]" nil ))nil ))nil 3397972136"" (skosimp)"" (expand "induced_measure" )"" (expand "restrict" ) (("" (propax) nil nil )) nil )) nil ))nil )"complete_measure" outer_measure_propsnil )"R" restrict nil ))nil 3408178896"" (expand "outer_negligible?" )"" (rewrite "m_outer_empty" ) nil nil )) nil )nil outer_measure_props nil )"bool" outer_measure_props nil ))nil ))nil 3408178896"" (skosimp)"" (typepred "n2!1" )"" (typepred "n1!1" )"" (expand "outer_negligible?" )"" "m_outer_subadditive" "A" "lambda i: if i = 0 then n1!1 elsif i=1 then n2!1 else emptyset[T] endif" ))"" "IUnion(LAMBDA i: IF i = 0 THEN n1!1") "1" (hide -1)"1" (name-replace "MM" "m(union[T](n1!1, n2!1))" )"1" (expand "o" )"1" (rewrite "m_outer_empty" )"1" (replace -2)"1" (replace -3)"1" "(LAMBDA (x: nat): IF x = 0 THEN (TRUE, 0)IF x = 1 THEN (TRUE, 0) ELSE (TRUE, 0) ENDIFlambda i:(TRUE,0)") "1" (hide -1 -3 -4)"1" expand "x_le" )"1" assert )"1" expand "x_sum" )"1" rewrite "zero_series_conv" )"1" rewrite "zero_series_limit" )"1" "1" assert )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (apply-extensionality :hide? t)"2" (case-replace "union[T](n1!1, n2!1)(x!1)" )"1" (expand "IUnion" )"1" (expand "union" )"1" (expand "member" )"1" (split)"1" (inst + "0" ) nil nil )"2" (inst + "1" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (replace 1 2)"2" (assert )"2" (expand "union" )"2" (flatten)"2" (expand "member" )"2" expand "IUnion" )"2" "2" assert )"2" expand "emptyset" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil outer_measure_propsnil )"bool" outer_measure_props nil )set type-eq-decl nil sets nil )nil outer_measure_props nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"set" sets nil )"set[T]" indexed_sets nil )"outer_measurable" nil )"outer_measurable" nil )"outer_measure" outer_measure_props nil )nil outer_measure_def nil )"bool" outer_measure_def nil )nil extended_nnreal"extended_nnreal/" )nil real_types nil )nil outer_measure_props nil )"(total_order?[real])" nil )nil series "series/" )nil series "series/" )"extended_nnreal" extended_nnreal"extended_nnreal/" )"bool" extended_nnreal "extended_nnreal/" )"bool" booleans nil )"T3" function_props nil )"bool" sets nil )"finite_set" finite_sets nil )"finite_set[T]" countable_props"sets_aux/" )"finite_set[T]" bounded_nats"orders/" )"finite_set[T]" countable_setofsets"sets_aux/" )"outer_negligible" nil )"(S)" outer_measure_propsnil )nil outer_measure_props nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )nil sequences nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"[T, T -> boolean]" equalities nil )"set" sets nil ))nil ))nil 3408178964"" (skosimp)"" (typepred "n!1" )"" (expand "outer_negligible?" )"" (lemma "m_outer_increasing" ("x" "x!1" "y" "n!1" ))"" (expand "x_le" )"" (assert )"" (replace -3)"" (replace -2)"" (assert )"" (flatten)"" (assert )"" (decompose-equality)"" (assert )"" (expand "<=" -3)"" assert )"" "m(x!1)`2" )"" assert )"" expand ">=" -1)"" expand "<=" -1)"" "1" assert )"1" "real_lt_is_strict_total_order" )"1" expand "strict_total_order?" )"1" expand "strict_order?" )"1" "1" expand "transitive?" )"1" "m(x!1)`2" "0" "m(x!1)`2" )"1" replace -4)"1" replace "1" expand "irreflexive?" )"1" "m(x!1)`2" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil outer_measure_propsnil )"bool" outer_measure_props nil )set type-eq-decl nil sets nil )nil outer_measure_props nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil outer_measure_props nil )"(partial_order?[set[T]])" nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil real_types nil )nil extended_nnreal"extended_nnreal/" )"bool" outer_measure_def nil )nil outer_measure_def nil )"outer_measure" outer_measure_props nil )"bool" booleans nil )"bool" reals nil )nil real_props nil )"bool" orders nil )"bool" relations nil )"bool" relations nil )"bool" orders nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"bool" extended_nnreal "extended_nnreal/" ))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.0.450Bemerkung:
(vorverarbeitet am 2026-05-01)
¤ *Bot Zugriff
2026-05-26
