Quelle lebesgue_def.prf
Sprache: Lisp
(lebesgue_defnil 3471434094"" (skosimp)"" (expand "member" )"" (expand "cal_M" )"" (lemma "outer_measurable_open_semi_infinite" ("a" "a!1" ))"" (expand "lebesgue_measurable" )"" (expand "fullset" )"" (expand "extend" ) (("" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" sets 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" sets nil )"R" extend nil )"sigma_algebra[real]" nil )"sigma_algebra" lebesgue_def nil ))nil 3471442368"" (expand "subset?" )"" (skosimp)"" (expand "member" )"" (expand "cal_M" )"" (expand "lebesgue_measurable" )"" (expand "fullset" )"" (expand "extend" )"" (prop)"" (lemma "borel_is_lebesgue_measurable" )"" (inst - "x!1" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"sigma_algebra" lebesgue_def nil )"set" sets nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )nil defined_types nil )nil sets nil )"bool" subset_algebra_def"measure_integration/" )nil subset_algebra_def"measure_integration/" )"bool" reals nil )nil real_types nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield, numfield -> numfield]" number_fields nil )"setofsets[T]" metric_space_def"metric_space/" )"sigma_algebra" borel "measure_integration/" )nil borel "measure_integration/" )"setof[real]" lebesgue_def nil )nil real_lebesgue_scafnil )"R" extend nil )"sigma_algebra[real]" nil )"bool" sets nil )"bool" sets nil ))nil 3471443245"" (expand "subset?" )"" (skosimp)"" (expand "member" )"" (lemma "borel_is_cal_M" )"" (expand "subset?" )"" (inst - "x!1" )"" (assert )"" (hide 2)"" (expand "borel?" )"" (expand "fullset" )"" (expand "extend" )"" "generated_sigma_algebra_subset1[real]" )"" "(LAMBDA (t: setof[real]): IF open?(t) THEN TRUE ELSE FALSE ENDIF)") "" (expand "subset?" )"" expand "member" )"" "x!1" )"" assert )"" "" expand "open_interval?" )"" "" rewrite "metric_open_def" )"" (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 lebesgue_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 booleans nil )nil defined_types nil )set type-eq-decl nil sets nil ) (fullset const-decl "set" sets nil )nil "measure_integration/" )nil metric_space "metric_space/" )"bool" real_intervals_aux nil )"bool" booleans nil )"bool" booleans nil )"bool" topology "topology/" )"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 )IF const-decl "[boolean, T, T -> T]" if_def nil )nil sets nil )"real" reals nil )"second_countable" real_topology "metric_space/" )"(hausdorff?)" "metric_space/" )"hausdorff[real]" "metric_space/" )"R" extend nil )"sigma_algebra" borel "measure_integration/" )"bool" sets nil )"bool" sets nil ))nil 3471443113"" (lemma "borel_is_cal_M" )"" (expand "subset?" )"" (skosimp)"" (inst - "x!1" )"" (expand "member" )"" (lemma "closed_is_borel" ("Y" "x!1" ))"1" (assert ) nil nil )"2" (expand "closed_interval?" )"2" (flatten)"2" (expand "closed?" )"2" (expand "metric_closed?" )"2" (expand "member" )"2" (expand "metric_induced_topology" )"2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" sets nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )nil defined_types nil )set type-eq-decl nil sets 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 sets nil )nil topology "topology/" )"bool" topology "topology/" )nil borel "measure_integration/" )"bool" metric_space_def "metric_space/" )"bool" real_intervals_aux nil )"bool" sets nil )nil lebesgue_def nil ))nil 3471441879"" (skosimp)"" (expand "member" )"" (expand "cal_M" )"" (expand "lebesgue_measurable" )"" (expand "fullset" )"" (expand "extend" )"" (assert )"" (lemma "borel_is_lebesgue_measurable" )"" (inst - "singleton[real](x!1)" )"1" (assert ) nil nil )"2" (rewrite "singleton_is_borel" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"non_empty_finite_set[T]" countable_setofsets "sets_aux/" )"closed[real, (metric_induced_topology)]" convergence_aux"metric_space/" )"compact[real, metric_induced_topology]" real_intervals nil )"bool" sets nil )"sigma_algebra[real]" nil )"R" extend nil )nil real_lebesgue_scafnil )nil hausdorff_borel"measure_integration/" )nil borel "measure_integration/" )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )nil defined_types nil )nil sets nil )"bool" subset_algebra_def"measure_integration/" )nil subset_algebra_def"measure_integration/" )"bool" reals nil )nil real_types nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield, numfield -> numfield]" number_fields nil )"setofsets[T]" metric_space_def"metric_space/" )"sigma_algebra" borel "measure_integration/" )set type-eq-decl nil sets nil )"bool" sets nil )"(singleton?)" sets nil )"real" lebesgue_def nil )"set" sets nil )"sigma_algebra" lebesgue_def nil ))nil 3471441715"" (skosimp)"" (lemma "open_interval_is_cal_M" )"" (expand "subset?" )"" (inst - "ball(x!1, r!1)" )"" (assert )"" (hide 2)"" (expand "open_interval?" )"" (expand "interval?" )"" (skosimp)"" (typepred "x!2" )"" (typepred "y!1" )"" (expand "ball" ) (("" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil lebesgue_def nil )"real" reals nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )set type-eq-decl nil sets nil ) (>= const-decl "bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield, numfield -> numfield]" number_fields nil )"set[T]" metric_space_def "metric_space/" )"bool" real_topology "metric_space/" )NOT const-decl "[bool -> bool]" booleans nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"bool" real_intervals_aux nil )"bool" sets nil )"metric_open[real, (LAMBDA (x, y: real): abs(x - y))]" "metric_space/" )"bool" sets nil ))nil 3471442240"" (skosimp)"" (expand "member" )"" (expand "cal_M" )"" (expand "lebesgue_measurable" )"" (expand "fullset" )"" (expand "extend" )"" (lemma "borel_is_lebesgue_measurable" )"" (inst - "closed_ball(x!1, nnr!1)" )"1" (assert ) nil nil )"2" (hide 2)"2" "closed_is_borel" "Y" "closed_ball(x!1, nnr!1)" ))"2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" sets nil )"sigma_algebra[real]" nil )"R" extend nil )"nnreal" lebesgue_def nil )"real" lebesgue_def nil )"closed" real_topology "metric_space/" )nil topology "topology/" )"bool" topology "topology/" )set type-eq-decl nil sets nil )nil real_types nil )"sigma_algebra" borel "measure_integration/" )"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"measure_integration/" )"bool" subset_algebra_def"measure_integration/" )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 borel "measure_integration/" )nil borel "measure_integration/" )nil real_lebesgue_scafnil )"set" sets nil )"sigma_algebra" lebesgue_def nil ))nil 3458582664"" (split)"1" (expand "cal_M" ) (("1" (propax) nil nil )) nil )"2" (typepred "lebesgue_measure" )"2" (expand "complete_sigma_finite?" )"2" (flatten)"2" (split)"1" (expand "measure?" )"1" (flatten)"1" (split)"1" (expand "measure_empty?" )"1" (propax) nil nil )) nil )"2" (expand "measure_countably_additive?" )"2" (skosimp)"2" (inst - "X!1" )"1" (expand "o " )"1" (expand "cal_M" )"1" (assert ) nil nil )) nil ))nil )"2" (hide 2)"2" (split)"1" (skosimp)"1" "X!1(x1!1)" )"1" expand "cal_M" )"1" (propax) nil nil ))nil ))nil ))nil )"2" (typepred "X!1" )"2" expand "disjoint_indexed_measurable?" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "measure_complete?" )"2" (skosimp)"2" (inst - "x!1" "a!1" )"2" (assert )"2" (expand "cal_M" )"2" (assert )"2" (expand "lebesgue_measure" )"2" (assert )"2" (split)"1" (propax) nil nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (expand "measure_sigma_finite?" )"3" (skosimp)"3" (inst + "X!1" )"1" (replace -3) (("1" (propax) nil nil )) nil )"2" (expand "cal_M" )"2" (typepred "X!1" )"2" (expand "disjoint_indexed_measurable?" )"2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"complete_sigma_finite[real, lebesgue_measurable]" nil )nil measure_def"measure_integration/" )"bool" measure_def"measure_integration/" )nil extended_nnreal"extended_nnreal/" )nil real_types nil )"bool" reals nil )"sigma_algebra[real]" nil )nil subset_algebra_def"measure_integration/" )"bool" subset_algebra_def"measure_integration/" )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 )"bool" measure_def"measure_integration/" )"disjoint_indexed_measurable[real, lebesgue_measurable]" nil )"bool" generalized_measure_def"measure_integration/" )set type-eq-decl nil sets nil )"(partial_order?[set[T]])" nil )"bool" generalized_measure_def"measure_integration/" )"bool" generalized_measure_def"measure_integration/" )"T3" function_props nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )"bool" "measure_integration/" )nil "measure_integration/" )"disjoint_indexed_measurable[real, cal_M]" nil )"bool" "measure_integration/" )"sigma_algebra" lebesgue_def nil ))nil ))nil 3475933087"" (skosimp)"" (lemma "singleton_is_cal_M" ("x" "x!1" ))"" (expand "member" ) (("" (propax) 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 lebesgue_def nil )"bool" sets nil ))nil ))nil 3475933229"" (skosimp)"" (expand "lambda_" )"" (lemma "lebesgue_outer_measure_singleton" ("x" "x!1" ))"" (expand "lebesgue_measure" )"" (expand "induced_measure" )"" (expand "restrict" )"" (expand "x_eq" )"" (flatten)"" (assert ) (("" (decompose-equality) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"complete_sigma_finite[real, cal_M]" nil )"complete_sigma_finite[real, lebesgue_measurable]" nil )"R" restrict nil )nil booleans nil )"bool" reals nil )nil real_types nil )set type-eq-decl nil sets nil )nil extended_nnreal"extended_nnreal/" )"bool" outer_measure_def"measure_integration/" )nil outer_measure_def"measure_integration/" )"outer_measure" nil )"bool" sets nil )"(singleton?)" sets nil )"bool" booleans nil )"non_empty_finite_set[T]" countable_setofsets "sets_aux/" )"closed[real, (metric_induced_topology)]" convergence_aux"metric_space/" )"compact[real, metric_induced_topology]" real_intervals nil )"bool" extended_nnreal "extended_nnreal/" )"complete_measure" outer_measure_props"measure_integration/" )nil nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil ))nil 3475932807"" (skosimp)"" (lemma "ball_is_cal_M" ("x" "x1!1" "r" "r!1" ))"" (expand "member" ) (("" (propax) nil nil )) nil )) nil ))nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals 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 lebesgue_def nil )"bool" sets nil ))nil ))nil 3475932807"" (skosimp)"" "lebesgue_outer_measure_bounded_interval" "b" "ball(x!1,r!1)" ))"1" (expand "lambda_" )"1" (expand "lebesgue_measure" )"1" (expand "induced_measure" )"1" (expand "restrict" )"1" (replace -1)"1" (hide -1)"1" (decompose-equality)"1" (expand "ball" )"1" "length_open_rew" "a" "x!1-r!1" "b" "x!1+r!1" ))"1" "{y: real | abs(x!1 - y) < r!1}={x | x!1 - r!1 < x AND x < x!1 + r!1}" )"1" (assert ) nil nil )"2" (apply-extensionality :hide? t)"2" (hide-all-but 1)"2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (expand "bounded_interval?" )"2" (split)"1" (grind) nil nil )"2" (expand "bounded?" )"2" (flatten)"2" (expand "nonempty?" )"2" (assert )"2" (hide 1)"2" (split)"1" (expand "above_bounded" )"1" (inst + "x!1+r!1" )"1" (grind) nil nil )) nil ))nil )"2" (expand "below_bounded" )"2" (inst + "x!1-r!1" )"2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))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 )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_topology"metric_space/" )"bool" real_topology "metric_space/" )set type-eq-decl nil sets 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 nil )"metric_open[real, (LAMBDA (x, y: real): abs(x - y))]" "metric_space/" )"real" reals nil )"complete_sigma_finite[real, lebesgue_measurable]" nil )"R" restrict nil )"bool" reals nil )"[T, T -> boolean]" equalities nil )"real" reals nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"[numfield, numfield -> numfield]" number_fields nil )"bool" reals nil )nil real_intervals_aux nil )"real" reals nil )nil real_types nil )"bool" booleans nil )"nnreal" real_intervals_aux nil )"[numfield, numfield -> numfield]" number_fields nil )"posreal" nil )"complete_measure" outer_measure_props"measure_integration/" )"complete_sigma_finite[real, cal_M]" nil )"bool" real_topology "metric_space/" )"bool" sets nil )"bool" bounded_reals "reals/" )"bool" bound_defs "reals/" )"bool" bounded_reals "reals/" )"bool" bound_defs "reals/" )"bool" real_topology "metric_space/" )NOT const-decl "[bool -> bool]" booleans nil ))nil 3475933226"" (skosimp)"" (lemma "closed_ball_is_cal_M" ("x" "x!1" "nnr" "nnr!1" ))"" (expand "member" ) (("" (propax) nil nil )) nil )) nil ))nil )nil real_types nil )"bool" reals 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 lebesgue_def nil )"bool" sets nil ))nil ))nil 3475933366"" (skosimp)"" (expand "lambda_" )"" (expand "lebesgue_measure" )"" (expand "induced_measure" )"" (expand "restrict" )"" "lebesgue_outer_measure_eq_length" "b" "closed_ball(x!1, nnr!1)" ))"1" "x_length(closed_ball(x!1, nnr!1))=(TRUE, 2 * nnr!1)" )"1" (hide -1)"1" (expand "x_eq" )"1" (flatten)"1" (assert )"1" (decompose-equality) nil nil )) nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (expand "x_length" )"2" (lift-if)"2" (assert )"2" (prop)"1" "length_closed_rew" "a" "x!1-nnr!1" "b" "x!1+nnr!1" ))"1" "closed_ball(x!1, nnr!1)={x | x!1 - nnr!1 <= x AND x <= x!1 + nnr!1}" )"1" (assert ) nil nil )"2" "2" "2" expand "closed_ball" )"2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "bounded_interval?" )"2" (split)"1" (grind) nil nil )"2" expand "bounded?" )"2" expand "nonempty?" )"2" "2" assert )"2" "2" "1" expand "above_bounded" )"1" "x!1+nnr!1" )"1" (grind) nil nil ))nil ))nil )"2" expand "below_bounded" )"2" "x!1-nnr!1" )"2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (expand "bounded_interval?" )"2" (split)"1" (grind) nil nil )"2" (expand "bounded?" )"2" (expand "nonempty?" )"2" (flatten)"2" (assert )"2" (hide 1)"2" "1" expand "above_bounded" )"1" "x!1+nnr!1" )"1" (grind) nil nil ))nil ))nil )"2" expand "below_bounded" )"2" "x!1-nnr!1" )"2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"complete_sigma_finite[real, cal_M]" nil )"complete_measure" outer_measure_props"measure_integration/" )"closed" real_topology "metric_space/" )nil topology "topology/" )"bool" topology "topology/" )"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 )nil sets nil )nil defined_types nil )nil real_types nil )"bool" reals nil )nil real_topology"metric_space/" )"bool" real_topology "metric_space/" )set type-eq-decl nil sets 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 nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"[numfield, numfield -> numfield]" number_fields nil )"bool" reals nil )nil real_intervals_aux nil )"real" reals nil )"real" reals nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" sets nil )"bool" bound_defs "reals/" )"bool" bounded_reals "reals/" )"bool" bound_defs "reals/" )"bool" bounded_reals "reals/" )"bool" real_topology "metric_space/" )"bool" outer_measure_def"measure_integration/" )nil outer_measure_def"measure_integration/" )"outer_measure" nil )"nnreal" nil )"bool" extended_nnreal "extended_nnreal/" )"[numfield, numfield -> numfield]" number_fields nil )"bool" booleans nil )"extended_nnreal" real_lebesgue_scaf nil )nil extended_nnreal"extended_nnreal/" )nil real_topology "metric_space/" )"bool" real_topology "metric_space/" )"[T, T -> boolean]" equalities nil )"R" restrict nil )"complete_sigma_finite[real, lebesgue_measurable]" nil ))nil 3475932141"" (skosimp)"" (rewrite "isf_is_integrable" )"" (hide 2)"" "isf_phi[real, cal_M, lambda_]" "E" "open(a!1, b!1)" ))"1" (propax) nil nil )"2" (hide 2)"2" "lambda_ball" "x" "(b!1+a!1)/2" "r" "(b!1-a!1)/2" ))"2" "ball_is_cal_M" "x" "(b!1+a!1)/2" "r" "(b!1-a!1)/2" ))"2" (expand "member" )"2" (expand "measurable_set?" )"2" "open(a!1, b!1)=ball((b!1 + a!1) / 2, (b!1 - a!1) / 2)" )"1" (assert )"1" (replace -2)"1" (expand "mu_fin?" )"1" (replace -3) (("1" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (apply-extensionality :hide? t)"2" (expand "open" )"2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil integral"measure_integration/" )"bool" isf "measure_integration/" )nil isf "measure_integration/" )set type-eq-decl nil sets nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )"nat" measure_space "measure_integration/" )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"[T, T -> boolean]" equalities nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield, numfield -> numfield]" number_fields nil )"set[T]" metric_space_def "metric_space/" )nil real_topology"metric_space/" )"open_interval" real_topology "metric_space/" )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )nil defined_types nil )nil sets nil )"bool" subset_algebra_def"measure_integration/" )nil subset_algebra_def"measure_integration/" )"sigma_algebra" lebesgue_def nil )"bool" reals nil )nil real_types nil )nil extended_nnreal"extended_nnreal/" )"bool" measure_def"measure_integration/" )nil measure_def"measure_integration/" )"complete_sigma_finite[real, cal_M]" nil )nil isf "measure_integration/" )"bool" measure_space_def"measure_integration/" )nil measure_space_def"measure_integration/" )"bool" measure_props "measure_integration/" )"real" reals nil )nil lebesgue_def nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"(total_order?[real])" nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"bool" sets nil )"metric_open[real, (LAMBDA (x, y: real): abs(x - y))]" "metric_space/" )"real" reals nil )"real" reals nil )nil lebesgue_def nil ))nil 3475934373"" (skosimp)"" "closed(a!1, b!1)=closed_ball((b!1+a!1)/2,(b!1-a!1)/2)" )"1" (hide -1)"1" "lambda_closed_ball" "x" "(b!1 + a!1) / 2" "nnr" "(b!1 - a!1) / 2" ))"1" "closed_ball_is_cal_M" "x" "(b!1 + a!1) / 2" "nnr" "(b!1 - a!1) / 2" ))"1" (expand "member" )"1" (rewrite "isf_is_integrable" +)"1" (hide 2)"1" (rewrite "isf_phi" )"1" (hide 2)"1" (expand "measurable_set?" )"1" (replace -1)"1" (expand "mu_fin?" )"1" (replace -2) (("1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (apply-extensionality :hide? t)"2" (expand "closed" ) (("2" (propax) nil nil )) nil )) nil ))nil ))nil )"real" reals nil )"(total_order?[real])" nil )"real" reals nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )set type-eq-decl nil sets nil )"[T, T -> boolean]" equalities nil )"bool" reals nil ) (>= const-decl "bool" reals nil )nil real_types nil )nil defined_types nil )nil sets nil )nil real_types nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield, numfield -> numfield]" number_fields nil )"setofsets[T]" metric_space_def"metric_space/" )"bool" topology "topology/" )nil topology "topology/" )"closed" real_topology "metric_space/" )nil real_topology"metric_space/" )"closed_interval" real_topology "metric_space/" )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil lebesgue_def nil )"bool" sets nil )nil isf "measure_integration/" )"bool" measure_space_def"measure_integration/" )nil measure_space_def"measure_integration/" )"bool" measure_props "measure_integration/" )"real" reals nil )"complete_sigma_finite[real, cal_M]" nil )nil measure_def"measure_integration/" )"bool" measure_def"measure_integration/" )nil extended_nnreal"extended_nnreal/" )"sigma_algebra" lebesgue_def nil )nil subset_algebra_def"measure_integration/" )"bool" subset_algebra_def"measure_integration/" )"nat" measure_space "measure_integration/" )nil naturalnumbers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil isf "measure_integration/" )"bool" isf "measure_integration/" )nil integral"measure_integration/" )"real" reals nil )nil lebesgue_def nil ))nil 3475932041"" (skosimp) (("" (rewrite "integrable_phi_open" ) nil nil )) nil )nil lebesgue_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 booleans nil )"bool" reals nil ))nil ))nil 3475934094"" (skosimp)"" "open(a!1, b!1)=ball((b!1 + a!1) / 2, (b!1 - a!1) / 2)" )"1" (hide -1)"1" "lambda_ball" "x" "(b!1 + a!1) / 2" "r" "(b!1 - a!1) / 2" ))"1" "ball_is_cal_M" "x" "(b!1 + a!1) / 2" "r" "(b!1 - a!1) / 2" ))"1" (expand "member" )"1" (rewrite "integral_phi" )"1" (expand "mu" )"1" (replace -2) (("1" (assert ) nil nil )) nil ))nil )"2" (expand "measurable_set?" )"2" (replace -1)"2" (expand "mu_fin?" )"2" (replace -2) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (apply-extensionality :hide? t)"2" (expand "open" ) (("2" (propax) nil nil )) nil )) nil ))nil ))nil ))nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"real" reals nil )"metric_open[real, (LAMBDA (x, y: real): abs(x - y))]" "metric_space/" )"real" reals nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )set type-eq-decl nil sets nil )"[T, T -> boolean]" equalities nil )"bool" reals nil ) (>= const-decl "bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield, numfield -> numfield]" number_fields nil )"set[T]" metric_space_def "metric_space/" )nil real_topology"metric_space/" )"open_interval" real_topology "metric_space/" )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil lebesgue_def nil )"bool" sets nil )"nnreal" measure_props "measure_integration/" )"real" reals nil )"complete_sigma_finite[real, cal_M]" nil )nil measure_def"measure_integration/" )"bool" measure_def"measure_integration/" )nil extended_nnreal"extended_nnreal/" )nil real_types nil )"sigma_algebra" lebesgue_def nil )nil subset_algebra_def"measure_integration/" )"bool" subset_algebra_def"measure_integration/" )nil sets nil )nil defined_types nil )"bool" measure_props "measure_integration/" )nil measure_space_def"measure_integration/" )"bool" measure_space_def"measure_integration/" )nil integral "measure_integration/" )"real" reals nil )nil lebesgue_def nil ))nil 3475932041"" (skosimp) (("" (rewrite "integrable_phi_closed" ) nil nil )) nil )nil lebesgue_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 booleans nil )"bool" reals nil ))nil ))nil 3475934559"" (skosimp)"" "closed(a!1, b!1)=closed_ball((b!1+a!1)/2,(b!1-a!1)/2)" )"1" (hide -1)"1" "lambda_closed_ball" "x" "(b!1 + a!1) / 2" "nnr" "(b!1 - a!1) / 2" ))"1" "closed_ball_is_cal_M" "x" "(b!1 + a!1) / 2" "nnr" "(b!1 - a!1) / 2" ))"1" (expand "member" )"1" (rewrite "integral_phi" )"1" (expand "mu" )"1" (replace -2) (("1" (assert ) nil nil )) nil ))nil )"2" (expand "mu_fin?" )"2" (replace -2)"2" (assert )"2" (expand "measurable_set?" )"2" (replace -1) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (apply-extensionality :hide? t)"2" (expand "closed" ) (("2" (propax) nil nil )) nil )) nil ))nil ))nil )"real" reals nil )"(total_order?[real])" nil )"real" reals nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )set type-eq-decl nil sets nil )"[T, T -> boolean]" equalities nil )"bool" reals nil ) (>= const-decl "bool" reals nil )nil real_types nil )nil defined_types nil )nil sets nil )nil real_types nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield, numfield -> numfield]" number_fields nil )"setofsets[T]" metric_space_def"metric_space/" )"bool" topology "topology/" )nil topology "topology/" )"closed" real_topology "metric_space/" )nil real_topology"metric_space/" )"closed_interval" real_topology "metric_space/" )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil lebesgue_def nil )"bool" sets nil )"nnreal" measure_props "measure_integration/" )"real" reals nil )"complete_sigma_finite[real, cal_M]" nil )nil measure_def"measure_integration/" )"bool" measure_def"measure_integration/" )nil extended_nnreal"extended_nnreal/" )"sigma_algebra" lebesgue_def nil )nil subset_algebra_def"measure_integration/" )"bool" subset_algebra_def"measure_integration/" )"bool" measure_props "measure_integration/" )nil measure_space_def"measure_integration/" )"bool" measure_space_def"measure_integration/" )nil integral "measure_integration/" )"real" reals nil )nil lebesgue_def nil ))nil 3475936049"" (rewrite "measurable_def2" )"" (skosimp)"" (typepred "i!1" )"" (skosimp)"" (lemma "ball_is_cal_M" ("x" "x!1" "r" "r!1" ))"" (expand "member" )"" (case-replace "inverse_image(I[real], i!1)=i!1" )"1" (assert ) nil nil )"2" (hide-all-but 1)"2" (apply-extensionality :hide? t)"2" (expand "inverse_image" )"2" (expand "member" )"2" (expand "I" ) (("2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" sets nil )"metric_open[real, (LAMBDA (x, y: real): abs(x - y))]" "metric_space/" )"continuous[real, metric_induced_topology, real, metric_induced_topology]" nil )"set[D]" function_image nil )nil lebesgue_def nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )set type-eq-decl nil sets nil )"[T, T -> boolean]" equalities nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield, numfield -> numfield]" number_fields nil )"set[T]" metric_space_def "metric_space/" )nil real_topology"metric_space/" )"sigma_algebra" lebesgue_def nil )nil subset_algebra_def"measure_integration/" )"bool" subset_algebra_def"measure_integration/" )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 )"(bijective?[T, T])" identity nil )"bool" functions nil )nil measure_space_def"measure_integration/" ))nil ))nil 3475936049"" (skolem + "f!1" )"" (typepred "f!1" )"" (lemma "I_is_measurable" )"" (lemma "continuous_is_borel" )"" (inst - "f!1" )"" "borel_comp_measurable_is_measurable" "phi" "f!1" "g" "I[real]" ))"1" (expand "o" )"1" "(LAMBDA (x: real): f!1(I[real](x)))=f!1" )"1" (hide-all-but 1)"1" (apply-extensionality :hide? t)"1" (grind) nil nil )) nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )nil continuity_def "topology/" )"bool" continuity_def "topology/" )"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 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 )nil borel_functions"measure_integration/" )"sigma_algebra" lebesgue_def nil )nil subset_algebra_def"measure_integration/" )"bool" subset_algebra_def"measure_integration/" )nil borel_functions"measure_integration/" )"bool" borel_functions"measure_integration/" )"(bijective?[T, T])" identity nil )"bool" functions nil )nil measure_space_def"measure_integration/" )"bool" measure_space_def"measure_integration/" )nil "measure_integration/" )"continuous[real, metric_induced_topology, real, metric_induced_topology]" nil )"measurable_function" lebesgue_defnil )"[T, T -> boolean]" equalities nil )"real" reals nil )"T3" function_props nil )nil lebesgue_def nil ))nil ))nil 3475936361"" (skosimp)"" (expand "measurable_set?" )"" (lemma "singleton_is_cal_M" ("x" "x!1" ))"" (expand "member" ) (("" (propax) nil nil )) nil )) nil ))nil ))nil )"non_empty_finite_set[real]" measure_space "measure_integration/" )"closed[real, (metric_induced_topology)]" convergence_aux"metric_space/" )"compact[real, metric_induced_topology]" real_intervals nil )"bool" measure_space_def"measure_integration/" )"bool" sets nil )nil lebesgue_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 ))nil 3475936361"" (skosimp)"" (expand "measurable_set?" )"" "ball_is_cal_M" ("x" "(b!1+a!1)/2" "r" "(b!1-a!1)/2" ))"" (expand "member" )"" "open(a!1, b!1)=ball((a!1 + b!1) / 2, (b!1 - a!1) / 2)" )"" (hide-all-but 1)"" (apply-extensionality :hide? t)"" (expand "open" ) (("" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" measure_space_def"measure_integration/" )"bool" sets nil )"real" reals nil )"open_interval" real_topology "metric_space/" )nil real_topology"metric_space/" )"set[T]" metric_space_def "metric_space/" )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )"[T, T -> boolean]" equalities nil )set type-eq-decl nil sets nil )"metric_open[real, (LAMBDA (x, y: real): abs(x - y))]" "metric_space/" )AND const-decl "[bool, bool -> bool]" booleans nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"(total_order?[real])" nil )"real" reals nil )nil lebesgue_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 booleans nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"bool" reals nil )"[numfield, numfield -> numfield]" number_fieldsnil ))nil ))nil 3475936361"" (skosimp)"" (expand "measurable_set?" )"" "closed_ball_is_cal_M" "x" "(b!1+a!1)/2" "nnr" "(b!1-a!1)/2" ))"" (expand "member" )"" "closed(a!1, b!1)=closed_ball((a!1 + b!1) / 2, (b!1 - a!1) / 2)" )"" (apply-extensionality :hide? t)"" (expand "closed" ) (("" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" measure_space_def"measure_integration/" )"bool" sets nil )"real" reals nil )"closed_interval" real_topology "metric_space/" )nil real_topology"metric_space/" )"closed" real_topology "metric_space/" )nil topology "topology/" )"bool" topology "topology/" )"setofsets[T]" metric_space_def"metric_space/" )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )nil sets nil )nil defined_types nil )"[T, T -> boolean]" equalities nil )set type-eq-decl nil sets nil )"real" reals nil )"(total_order?[real])" nil )"real" reals nil )nil lebesgue_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 booleans nil )"bool" reals nil )nil real_types nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"bool" reals nil )"[numfield, numfield -> numfield]" number_fieldsnil ))nil ))nil 3475936361"" case "forall (n:nat,X:finite_set[real]): card(X) <= n => ") "1" (skosimp)"1" (inst - "card(x!1)" "x!1" ) (("1" (assert ) nil nil )) nil ))nil )"2" (hide 2)"2" (induct "n" )"1" (skosimp)"1" (expand "<=" )"1" (split)"1" (assert ) nil nil )"2" (lemma "card_is_0[real]" ("S" "X!1" ))"2" (assert )"2" (replace -2)"2" (replace -1)"2" (hide -1 -2)"2" (assert )"2" (expand "measurable_set?" )"2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (expand "<=" -2)"2" (split -2)"1" (inst - "X!1" ) (("1" (assert ) nil nil )) nil )"2" (lemma "nonempty_card[real]" ("S" "X!1" ))"2" (assert )"2" (copy -1)"2" (expand "nonempty?" -1)"2" (lemma "card_rest[real]" ("S" "X!1" ))"2" (assert )"2" (replace -3)"2" (assert )"2" "rest[real](X!1)" )"2" assert )"2" "singleton_is_measurable" "x" "choose[real](X!1)" ))"2" "choose_rest[real]" "a" "X!1" ))"2" assert )"2" rewrite "add_as_union" )"2" "cal_M" )"2" "sigma_algebra_union[real,cal_M]" "x" "rest[real](X!1)" "y" "singleton[real](choose[real](X!1))" ))"1" expand "member" )"1" expand "measurable_set?" )"1" assert )nil nil ))nil ))nil )"2" expand "measurable_set?" )"2" nil nil ))nil )"3" expand "measurable_set?" )"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 ))nil )"posint" nil )"(strict_total_order?[real])" real_props nil )"bool" sets nil )"int" integers nil )"finite_set[real]" measure_space"measure_integration/" )nil sets_lemmas nil )nil sets_lemmas nil )"non_empty_finite_set[real]" measure_space "measure_integration/" )"finite_set[real]" "measure_integration/" )nil sigma_algebra"measure_integration/" )"bool" sets nil )"(singleton?)" sets nil )"bool" sets nil )NOT const-decl "[bool -> bool]" booleans nil )"measurable_set" nil )"non_empty_finite_set[real]" measure_space "measure_integration/" )"closed[real, (metric_induced_topology)]" convergence_aux"metric_space/" )"compact[real, metric_induced_topology]" real_intervals nil )"(p)" sets nil )nil lebesgue_def nil )"set" sets nil )nil finite_sets nil )nil finite_sets nil )"(strict_total_order?[real])" real_props nil )"(lebesgue_measurable)" nil )"(borel?)" real_borel"measure_integration/" )"(induced_sigma_algebra)" nil )"outer_negligible[real, lebesgue_outer_measure]" nil )"clopen[real, (metric_induced_topology)]" real_topology"metric_space/" )"compact[real, (metric_induced_topology)]" real_topology"metric_space/" )"(cal_M)" lebesgue_def nil )"null_set[real, cal_M, lambda_]" nil )"finite_set[real]" measure_space"measure_integration/" )"finite_set[T]" countable_setofsets"sets_aux/" )"finite_set[T]" countable_props"sets_aux/" )"finite_set[T]" bounded_nats"orders/" )"finite_set[T]" sigma_countable"sigma_set/" )"finite_set" finite_sets nil )nil finite_sets nil )nil naturalnumbers nil )nil defined_types nil )"(total_order?[real])" 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 )set type-eq-decl nil sets nil )"bool" finite_sets nil )nil finite_sets nil )"[bool, bool -> bool]" booleans nil )"bool" reals nil )"[T, T -> boolean]" equalities nil )"nat" finite_sets nil )"{n: nat | n = Card(S)}" finite_sets nil )nil defined_types nil )nil sets nil )"bool" subset_algebra_def"measure_integration/" )nil subset_algebra_def"measure_integration/" )"sigma_algebra" lebesgue_def nil )"bool" measure_space_def"measure_integration/" ))nil ))nil 3475936581"" (skosimp)"" (typepred "x!1" )"" (rewrite "countable_card" -1)"" (split)"1" (lemma "finite_is_measurable" )"1" (inst - "x!1" ) nil nil )) nil )"2" (expand "is_countably_infinite" )"2" (skosimp)"2" (typepred "f!1" )"2" "bijective_inverse_exists[(x!1), nat]" "f" "f!1" ))"2" (expand "exists1" )"2" (flatten)"2" (skolem - "g!1" )"2" "measurable_IUnion" "SS" "singleton[real] o g!1" ))"1" "(IUnion[nat, real](singleton[real] o g!1))=x!1" )"1" (apply-extensionality :hide? t)"1" expand "o " )"1" expand "singleton" )"1" expand "IUnion" )"1" "x!1(x!2)" )"1" "f!1(x!2)" )"1" rewrite "comp_inverse_left_alt[(x!1), nat]" )nil nil ))nil )"2" assert )"2" "2" replace -1)"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "o" )"2" (skosimp)"2" rewrite "singleton_is_measurable" )nil nil ))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 )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 )nil finite_sets nil )"bool" finite_sets nil )"countable_set[real]" lebesgue_def nil )nil lebesgue_def nil )nil function_inverse_defnil )"sigma_algebra" lebesgue_def nil )nil subset_algebra_def"measure_integration/" )"bool" subset_algebra_def"measure_integration/" )nil sets nil )nil defined_types nil )"(singleton?)" sets nil )"T3" function_props nil )"bool" sets nil )nil sequences nil )nil measure_space_def"measure_integration/" )"bool" measure_space_def"measure_integration/" )nil measure_space_def"measure_integration/" )"bool" function_inverse_def nil )nil function_inverse_def nil )"real" lebesgue_def nil )"[T, T -> boolean]" equalities nil )"set[T]" indexed_sets nil )nil lebesgue_def nil )"compact[real, metric_induced_topology]" real_intervals nil )"closed[real, (metric_induced_topology)]" convergence_aux"metric_space/" )"non_empty_finite_set[real]" measure_space "measure_integration/" )"measurable_set" nil )"bool" exists1 nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" functions nil )"bool" countability "sets_aux/" )nil countable_props "sets_aux/" ))nil ))nil 3475936361"" (skosimp)"" (expand "null_set?" )"" (rewrite "singleton_is_measurable" )"" (expand "mu_fin?" )"" (expand "mu" )"" (lemma "lambda_singleton" ("x" "x!1" ))"" (replace -1) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil )"measurable_set" nil )"non_empty_finite_set[real]" measure_space "measure_integration/" )"closed[real, (metric_induced_topology)]" convergence_aux"metric_space/" )"compact[real, metric_induced_topology]" real_intervals nil )"bool" measure_theory "measure_integration/" )"bool" measure_props "measure_integration/" )nil lebesgue_def nil )"nnreal" measure_props "measure_integration/" )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil lebesgue_def nil ))nil ))nil 3475936361"" case "forall (X:finite_set[real],n:nat): card[real](X) <= n => null_set?[real, cal_M, lambda_](X)" )"1" (skosimp)"1" (inst - "x!1" "card(x!1)" ) (("1" (assert ) nil nil )) nil ))nil )"2" (hide 2)"2" (induct "n" )"1" (skosimp)"1" (expand "<=" )"1" (split)"1" (assert ) nil nil )"2" (rewrite "card_is_0" )"2" (replace -1)"2" (hide -1)"2" (rewrite "null_emptyset" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (expand "<=" -2)"2" (split)"1" (inst - "X!1" ) (("1" (assert ) nil nil )) nil )"2" (lemma "nonempty_card[real]" ("S" "X!1" ))"2" (assert )"2" (copy -1)"2" (expand "nonempty?" -1)"2" (lemma "card_rest[real]" ("S" "X!1" ))"2" (assert )"2" (replace -3)"2" (assert )"2" "rest[real](X!1)" )"2" assert )"2" "singleton_is_null" "x" "choose[real](X!1)" ))"2" "choose_rest[real]" "a" "X!1" ))"2" assert )"2" rewrite "add_as_union" )"2" replace -1 2 rl)"2" "null_union" "N1" "rest[real](X!1)" "N2" "singleton[real](choose[real](X!1))" ))"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"posint" nil )"(strict_total_order?[real])" real_props nil )"bool" sets nil )"int" integers nil )"finite_set[real]" measure_space"measure_integration/" )nil sets_lemmas nil )nil sets_lemmas nil )"non_empty_finite_set[real]" measure_space "measure_integration/" )"finite_set[real]" "measure_integration/" )nil measure_theory"measure_integration/" )nil measure_theory"measure_integration/" )"bool" sets nil )"(singleton?)" sets nil )"null_set" lebesgue_defnil )"non_empty_finite_set[real]" measure_space "measure_integration/" )"closed[real, (metric_induced_topology)]" convergence_aux"metric_space/" )"compact[real, metric_induced_topology]" real_intervals nil )"(p)" sets nil )nil lebesgue_def nil )"set" sets nil )nil finite_sets nil )nil finite_sets nil )"(strict_total_order?[real])" real_props nil )nil measure_theory"measure_integration/" )"finite_set" finite_sets nil )"finite_set[T]" sigma_countable"sigma_set/" )"finite_set[T]" bounded_nats"orders/" )"finite_set[T]" countable_props"sets_aux/" )"finite_set[T]" countable_setofsets"sets_aux/" )"finite_set[real]" measure_space"measure_integration/" )"null_set[real, cal_M, lambda_]" nil )"(cal_M)" lebesgue_def nil )"compact[real, (metric_induced_topology)]" real_topology"metric_space/" )"clopen[real, (metric_induced_topology)]" real_topology"metric_space/" )"outer_negligible[real, lebesgue_outer_measure]" nil )"(induced_sigma_algebra)" nil )"(borel?)" real_borel"measure_integration/" )"(lebesgue_measurable)" nil )nil finite_sets nil )nil naturalnumbers nil )nil defined_types nil )"(total_order?[real])" nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )set type-eq-decl nil sets nil )"bool" finite_sets nil )nil finite_sets nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"[bool, bool -> bool]" booleans nil )"bool" reals nil )"[T, T -> boolean]" equalities nil )"nat" finite_sets nil )"{n: nat | n = Card(S)}" finite_sets nil )nil defined_types nil )nil sets nil )"bool" subset_algebra_def"measure_integration/" )nil subset_algebra_def"measure_integration/" )"sigma_algebra" lebesgue_def nil )nil real_types nil )nil extended_nnreal"extended_nnreal/" )"bool" measure_def"measure_integration/" )nil measure_def"measure_integration/" )"complete_sigma_finite[real, cal_M]" nil )"bool" measure_theory"measure_integration/" ))nil ))nil 3475936361"" (skosimp)"" (typepred "x!1" )"" (rewrite "countable_card" -1)"" (split)"1" (rewrite "finite_is_null" ) nil nil )"2" (expand "is_countably_infinite" )"2" (skosimp)"2" (typepred "f!1" )"2" "bijective_inverse_exists[(x!1), nat]" "f" "f!1" ))"2" (expand "exists1" )"2" (flatten)"2" (skolem - "g!1" )"2" "null_IUnion" "NS" "singleton[real] o g!1" ))"1" "(IUnion[nat, real](singleton[real] o g!1))=x!1" )"1" (hide -1 2)"1" "1" expand "o " )"1" expand "IUnion" )"1" expand "singleton" )"1" "x!1(x!2)" )"1" "f!1(x!2)" )"1" rewrite "comp_inverse_left_alt[(x!1), nat]" )nil nil ))nil )"2" assert )"2" "2" replace -1)"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "o" )"2" (skosimp)"2" "singleton_is_null" "x" "g!1(x1!1)" ))"2" (propax) nil nil ))nil ))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 )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 )nil finite_sets nil )"bool" finite_sets nil )nil lebesgue_def nil )nil function_inverse_defnil )"complete_sigma_finite[real, cal_M]" nil )nil measure_def"measure_integration/" )"bool" measure_def"measure_integration/" )nil extended_nnreal"extended_nnreal/" )nil real_types nil )"sigma_algebra" lebesgue_def nil )nil subset_algebra_def"measure_integration/" )"bool" subset_algebra_def"measure_integration/" )nil sets nil )nil defined_types nil )"(singleton?)" sets nil )"T3" function_props nil )"bool" sets nil )nil sequences nil )nil measure_theory"measure_integration/" )"bool" measure_theory "measure_integration/" )nil measure_theory"measure_integration/" )"countable_set[real]" lebesgue_def nil )"real" lebesgue_def nil )nil function_inverse_def nil )"bool" function_inverse_def nil )"[T, T -> boolean]" equalities nil )"set[T]" indexed_sets nil )nil lebesgue_def nil )"compact[real, metric_induced_topology]" real_intervals nil )"closed[real, (metric_induced_topology)]" convergence_aux"metric_space/" )"non_empty_finite_set[real]" measure_space "measure_integration/" )"null_set" lebesgue_defnil )"bool" exists1 nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" functions nil )"bool" countability "sets_aux/" )nil countable_props "sets_aux/" ))nil ))nil 3475937385"" (skosimp)"" (lemma "integrable_phi_closed" ("a" "x!1" "b" "x!1" ))"" (case-replace "closed(x!1,x!1)=singleton[real](x!1)" )"" (hide-all-but 1)"" (apply-extensionality :hide? t) (("" (grind) nil nil ))nil ))nil ))nil ))nil ))nil )"bool" reals 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 lebesgue_def nil )"(total_order?[real])" nil )"real" reals nil )"real" reals nil )"real" reals nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"(singleton?)" sets nil )"bool" sets nil )"closed_interval" real_topology "metric_space/" )nil real_topology"metric_space/" )"closed" real_topology "metric_space/" )nil topology "topology/" )"bool" topology "topology/" )"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 )nil sets nil )nil defined_types nil )nil real_types nil )"bool" reals nil )"[T, T -> boolean]" equalities nil )set type-eq-decl nil sets nil )"compact[real, metric_induced_topology]" real_intervals nil )"closed[real, (metric_induced_topology)]" convergence_aux"metric_space/" )"non_empty_finite_set[real]" measure_space "measure_integration/" )"null_set" lebesgue_defnil )"measurable_set" nil ))nil 3475940248"" case "forall (n:nat,X: finite_set[real]): card(X) <= n => integrable?(phi(X))" )"1" (skosimp)"1" (inst - "card(X!1)" "X!1" ) (("1" (assert ) nil nil )) nil ))nil )"2" (hide 2)"2" (induct "n" )"1" (skosimp)"1" (expand "<=" )"1" (split)"1" (assert ) nil nil )"2" (rewrite "card_is_0" )"2" (replace -1)"2" (hide -1)"2" "phi(emptyset[real])=lambda x: 0" )"1" (rewrite "integrable_zero" ) nil nil )"2" (apply-extensionality :hide? t)"2" (expand "emptyset" )"2" (expand "phi" )"2" (expand "member" )"2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (expand "<=" -2)"2" (split)"1" (inst - "X!1" ) (("1" (assert ) nil nil )) nil )"2" (lemma "nonempty_card[real]" ("S" "X!1" ))"2" (assert )"2" (lemma "card_rest[real]" ("S" "X!1" ))"2" (split)"1" (inst - "rest[real](X!1)" )"1" (assert )"1" (lemma "choose_rest[real]" ("a" "X!1" ))"1" (split)"1" rewrite "add_as_union" )"1" "integrable_singleton" "x" "choose[real](X!1)" ))"1" replace -2 1 rl)"1" "integrable_add" "f1" "phi(rest[real](X!1))" "f2" "phi(singleton[real](choose[real](X!1)))" ))"1" expand "+" -1)"1" "(LAMBDA (x: real): leton[real](choose[real](X!1))))") "1" "1" "1" expand "phi" )"1" expand "union" )"1" expand "member" )"1" expand "singleton" )"1" "rest[real](X!1)(x!1)" )"1" "choose_not_member[real]" "a" "X!1" ))"1" "1" assert )nil nil )"2" expand "nonempty?" )"2" assert )nil nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil )"2" expand "nonempty?" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "nonempty?" )"2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"posint" nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )nil lebesgue_def nil )nil integral "measure_integration/" )nil integral"measure_integration/" )"bool" sets nil )"(singleton?)" sets nil )"set" sets nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"nonneg_int" nil )nil sets_lemmas nil )"[T -> real]" real_fun_ops "reals/" )"finite_set[real]" "measure_integration/" )"non_empty_finite_set[real]" measure_space "measure_integration/" )"null_set" lebesgue_defnil )"non_empty_finite_set[real]" measure_space "measure_integration/" )"closed[real, (metric_induced_topology)]" convergence_aux"metric_space/" )nil sets_lemmas nil )"bool" sets nil )"(p)" sets nil )nil sets_lemmas nil )"set" sets nil )"finite_set[real]" measure_space"measure_integration/" )nil finite_sets nil )nil finite_sets nil )"(strict_total_order?[real])" real_props nil )"set" sets nil )"simple[real, cal_M]" nil )nil integral "measure_integration/" )"bool" sets nil )"finite_set" finite_sets nil )"finite_set[T]" sigma_countable"sigma_set/" )"finite_set[T]" bounded_nats"orders/" )"finite_set[T]" countable_props"sets_aux/" )"finite_set[T]" countable_setofsets"sets_aux/" )"finite_set[real]" measure_space"measure_integration/" )"null_set[real, cal_M, lambda_]" nil )"(cal_M)" lebesgue_def nil )"compact[real, (metric_induced_topology)]" real_topology"metric_space/" )"clopen[real, (metric_induced_topology)]" real_topology"metric_space/" )"outer_negligible[real, lebesgue_outer_measure]" nil )"(induced_sigma_algebra)" nil )"(borel?)" real_borel"measure_integration/" )"(lebesgue_measurable)" nil )nil finite_sets nil )nil naturalnumbers nil )nil defined_types nil )"(total_order?[real])" 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 )set type-eq-decl nil sets nil )"bool" finite_sets nil )nil finite_sets nil )"[bool, bool -> bool]" booleans nil )"bool" reals nil )"[T, T -> boolean]" equalities nil )"nat" finite_sets nil )"{n: nat | n = Card(S)}" finite_sets nil )nil defined_types nil )nil sets nil )"bool" subset_algebra_def"measure_integration/" )nil subset_algebra_def"measure_integration/" )"sigma_algebra" lebesgue_def nil )nil real_types nil )nil extended_nnreal"extended_nnreal/" )"bool" measure_def"measure_integration/" )nil measure_def"measure_integration/" )"complete_sigma_finite[real, cal_M]" nil )"bool" integral "measure_integration/" )"nat" measure_space "measure_integration/" ))nil 3475940817"" (skosimp)"" (lemma "countable_is_null" )"" (inst - "C!1" )"" (expand "null_set?" )"" (flatten)"" (rewrite "isf_is_integrable" )"" (rewrite "isf_phi" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )nil lebesgue_def nil )"bool" measure_theory "measure_integration/" )nil integral"measure_integration/" )"bool" isf "measure_integration/" )nil isf "measure_integration/" )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )"nat" measure_space "measure_integration/" )nil defined_types nil )nil sets nil )"bool" subset_algebra_def"measure_integration/" )nil subset_algebra_def"measure_integration/" )"sigma_algebra" lebesgue_def nil )"bool" reals nil )nil real_types nil )nil extended_nnreal"extended_nnreal/" )"bool" measure_def"measure_integration/" )nil measure_def"measure_integration/" )"complete_sigma_finite[real, cal_M]" nil )nil isf "measure_integration/" )"bool" measure_space_def"measure_integration/" )nil measure_space_def"measure_integration/" )"bool" measure_props "measure_integration/" )nil countability "sets_aux/" )"bool" countability "sets_aux/" )set type-eq-decl nil sets 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 3475936361"" (skosimp) (("" (rewrite "integrable_singleton" ) nil nil )) nil )nil lebesgue_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 ))nil 3475941153"" (skosimp)"" (lemma "integral_phi_closed" ("a" "x!1" "b" "x!1" ))"" (case-replace "closed(x!1, x!1)=singleton[real](x!1)" )"1" (assert ) nil nil )"2" (apply-extensionality :hide? t)"2" (expand "closed" )"2" (hide-all-but 1)"2" (expand "singleton" )"2" (expand "closed_ball" ) (("2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" reals 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 lebesgue_def nil )"(total_order?[real])" nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"real" reals nil )"(singleton?)" sets nil )"bool" sets nil )"closed_interval" real_topology "metric_space/" )nil real_topology"metric_space/" )"closed" real_topology "metric_space/" )nil topology "topology/" )"bool" topology "topology/" )"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 )nil sets nil )nil defined_types nil )nil real_types nil )"bool" reals nil )"[T, T -> boolean]" equalities nil )set type-eq-decl nil sets nil )"compact[real, metric_induced_topology]" real_intervals nil )"closed[real, (metric_induced_topology)]" convergence_aux"metric_space/" )"non_empty_finite_set[real]" measure_space "measure_integration/" )"null_set" lebesgue_defnil )"measurable_set" nil ))nil 3475936361"" (skosimp) (("" (rewrite "integrable_finite" ) nil nil )) nil )nil lebesgue_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 booleans nil )set type-eq-decl nil sets nil )"bool" finite_sets nil )nil finite_sets nil ))nil ))nil 3475945770"" (skosimp)"" (lemma "finite_is_null" )"" (inst - "X!1" )"" (expand "null_set?" )"" (flatten) (("" (rewrite "integral_phi" ) nil nil )) nil ))nil ))nil ))nil ))nil )nil lebesgue_def nil )"bool" measure_theory "measure_integration/" )nil integral "measure_integration/" )"bool" measure_space_def"measure_integration/" )nil measure_space_def"measure_integration/" )"bool" measure_props "measure_integration/" )nil defined_types nil )nil sets nil )"bool" subset_algebra_def"measure_integration/" )nil subset_algebra_def"measure_integration/" )"sigma_algebra" lebesgue_def nil )"bool" reals nil )nil real_types nil )nil extended_nnreal"extended_nnreal/" )"bool" measure_def"measure_integration/" )nil measure_def"measure_integration/" )"complete_sigma_finite[real, cal_M]" nil )nil finite_sets nil )"bool" finite_sets nil )set type-eq-decl nil sets 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 3475936581"" (skosimp) (("" (rewrite "integrable_countable" ) nil nil )) nil )nil lebesgue_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 booleans nil )set type-eq-decl nil sets nil )"bool" countability "sets_aux/" )nil countability "sets_aux/" ))nil ))nil 3475945816"" (skosimp)"" (lemma "countable_is_null" )"" (inst - "C!1" )"" (expand "null_set?" )"" (flatten) (("" (rewrite "integral_phi" ) nil nil )) nil ))nil ))nil ))nil ))nil )nil lebesgue_def nil )"bool" measure_theory "measure_integration/" )nil integral "measure_integration/" )"bool" measure_space_def"measure_integration/" )nil measure_space_def"measure_integration/" )"bool" measure_props "measure_integration/" )nil defined_types nil )nil sets nil )"bool" subset_algebra_def"measure_integration/" )nil subset_algebra_def"measure_integration/" )"sigma_algebra" lebesgue_def nil )"bool" reals nil )nil real_types nil )nil extended_nnreal"extended_nnreal/" )"bool" measure_def"measure_integration/" )nil measure_def"measure_integration/" )"complete_sigma_finite[real, cal_M]" nil )nil countability "sets_aux/" )"bool" countability "sets_aux/" )set type-eq-decl nil sets 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 3475946220"" (skosimp)"" (typepred "b!1" )"" (expand "bounded_open_interval?" )"" (expand "bounded_interval?" )"" (expand "bounded?" )"" (flatten)"" (assert )"" (split)"1" (expand "nonempty?" ) (("1" (propax) nil nil ))nil )"2" (flatten)"2" (name "SUP" "sup(b!1)" )"1" (name "INF" "inf(b!1)" )"1" (typepred "inf(b!1)" )"1" (typepred "sup(b!1)" )"1" (replace -3)"1" replace -4)"1" "1" expand "least_upper_bound" )"1" expand "greatest_lower_bound" )"1" "1" expand "lower_bound" )"1" expand "upper_bound" )"1" case "FORALL (z: (b!1)): z < SUP" )"1" case "FORALL (z: (b!1)): INF<z" )"1" case "SUP>INF" )"1" "(SUP+INF)/2" "(SUP-INF)/2" )"1" "1" "b!1(x!1)" )"1" "x!1" )"1" "x!1" )"1" "1" nil nil ))nil ))nil ))nil )"2" assert )"2" case "INF<x!1& x!1<SUP" )"1" "1" "1" "x!1" )"1" assert )"1" "1" "x!1" )"1" assert )"1" "1" expand "interval?" )"1" "z!2" "z!1" "x!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil )"2" expand "nonempty?" )"2" expand "empty?" )"2" "2" assert )"2" "x!1" )"2" "x!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "z!1" )"2" expand "<=" "2" "1" nil nil )"2" expand "metric_open?" )"2" "z!1" )"2" assert )"2" "2" expand "subset?" )"2" expand "member" )"2" expand "ball" )"2" "z!1-r!1/2" )"2" assert )"2" expand "abs" )"2" "z!1-r!1/2" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "z!1" )"2" "z!1" )"2" expand "<=" -3)"2" "1" nil nil )"2" "2" expand "metric_open?" )"2" "z!1" )"2" assert )"2" "2" expand "subset?" )"2" expand "member" )"2" expand "ball" )"2" "z!1+r!1/2" )"2" assert )"2" rewrite "abs_mult" )"2" rewrite "abs_neg" )"2" expand "abs" )"2" "r!1/2+z!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 ))nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil real_topology"metric_space/" )"bool" real_topology"metric_space/" )set type-eq-decl nil sets 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 )"bool" real_topology "metric_space/" )"bool" sets nil )"{x | least_upper_bound(<=)(x, Su)}" bounded_reals"reals/" )"bool" reals nil )"bool" bound_defs "reals/" )nil defined_types nil )nil bounded_reals "reals/" )"bool" bounded_reals "reals/" )nil defined_types nil )"[T, T -> boolean]" equalities nil )"bool" bound_defs "reals/" )"bool" reals nil )"posreal" nil )"posreal" lebesgue_def nil )"(b!1)" lebesgue_def nil )"bool" sets nil )"bool" metric_space_def "metric_space/" )"bool" reals nil )"[numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"set[T]" metric_space_def "metric_space/" )"metric_open[real, (LAMBDA (x, y: real): abs(x - y))]" "metric_space/" )"real" reals nil )"real" reals nil )"(total_order?[real])" nil )"bool" real_topology "metric_space/" )"real" lebesgue_def nil )"(strict_total_order?[real])" real_props nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_types nil )nil real_types nil )"{x | greatest_lower_bound(<=)(x, b!1)}" nil )"{x | least_upper_bound(<=)(x, b!1)}" nil )"bounded_open_interval" lebesgue_def nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"real" reals nil )"(total_order?[real])" nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"bool" sets nil )"bool" sets nil )"nzreal" nil )nil real_props nil )"{y: posreal | y >= x}" nil )"{j: posint | j >= i}" nil )"posreal" nil )"posreal" lebesgue_def nil )"(b!1)" lebesgue_def nil )"nzint" integers nil )"bool" bound_defs "reals/" )"{x | greatest_lower_bound(<=)(x, Sl)}" "reals/" )"bool" bound_defs "reals/" )nil bounded_reals "reals/" )"bool" bounded_reals "reals/" )"bool" real_topology "metric_space/" ))nil 3475937691"" (skolem + "b!1" )"" (lemma "nonempty_bounded_open_interval_prop" ("b" "b!1" ))"" (typepred "b!1" )"" (expand "bounded_open_interval?" )"" (expand "bounded_interval?" )"" (flatten)"" (expand "bounded?" )"" (split)"1" (rewrite "emptyset_is_empty?" )"1" (replace -1)"1" (rewrite "measurable_emptyset" ) nil nil ))nil ))nil )"2" (flatten)"2" (assert )"2" (skosimp)"2" (replace -6)"2" "ball_is_cal_M" "x" "x!1" "r" "r!1" ))"2" (expand "member" )"2" expand "measurable_set?" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil real_topology"metric_space/" )"bool" real_topology"metric_space/" )set type-eq-decl nil sets 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 lebesgue_defnil )nil measure_space_def"measure_integration/" )nil defined_types nil )nil sets nil )"bool" subset_algebra_def"measure_integration/" )nil subset_algebra_def"measure_integration/" )"sigma_algebra" lebesgue_def nil )"finite_set" finite_sets nil )"finite_set[T]" sigma_countable"sigma_set/" )"finite_set[T]" bounded_nats"orders/" )"finite_set[T]" countable_props"sets_aux/" )"finite_set[T]" countable_setofsets"sets_aux/" )"finite_set[real]" measure_space"measure_integration/" )"null_set[real, cal_M, lambda_]" nil )"(cal_M)" lebesgue_def nil )"compact[real, (metric_induced_topology)]" real_topology"metric_space/" )"clopen[real, (metric_induced_topology)]" real_topology"metric_space/" )"outer_negligible[real, lebesgue_outer_measure]" nil )"(induced_sigma_algebra)" nil )"(borel?)" real_borel"measure_integration/" )"(lebesgue_measurable)" nil )nil sets_lemmas nil )"bool" sets nil )"bool" measure_space_def"measure_integration/" )"metric_open[real, (LAMBDA (x, y: real): abs(x - y))]" "metric_space/" )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil lebesgue_def nil )"bool" real_topology "metric_space/" )"bool" real_topology "metric_space/" )NOT const-decl "[bool -> bool]" booleans nil ))nil ))nil 3475937691"" (skosimp*)"" (lemma "measurable_IUnion" ("SS" "I!1" ))"" (expand "measurable_set?" )"" case "FORALL (n): ") "1" (inst - "n!1" )"1" (assert )"1" (expand "mu_fin?" )"1" "m_monotone" "a" "IUnion[real](n!1, I!1)" "b" "IUnion(I!1)" ))"1" (expand "x_le" )"1" (assert )"1" (hide-all-but 1)"1" (expand "IUnion" )"1" (expand "image" )"1" (expand "Union" )"1" expand "subset?" )"1" expand "member" )"1" "1" "a!1" )"1" "i!1" )"1" "i!1" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "measurable_set?" )"2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (hide 2 -1)"2" (induct "n" )"1" (rewrite "IUnion_0_def" )"1" (assert )"1" (lemma "bounded_open_interval_is_measurable" )"1" (inst - "I!1(0)" )"1" (expand "measurable_set?" )"1" (propax) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (skosimp)"2" (rewrite "IUnion_n_def" )"2" "measurable_union" "a" "IUnion(j!1, I!1)" "b" "I!1(1 + j!1)" ))"1" (expand "measurable_set?" )"1" (propax) nil nil )) nil )"2" (expand "measurable_set?" )"2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"sigma_algebra" lebesgue_def nil )nil subset_algebra_def"measure_integration/" )"bool" subset_algebra_def"measure_integration/" )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 real_topology"metric_space/" )"bool" real_topology"metric_space/" )nil sequences nil )nil measure_space_def"measure_integration/" )"bool" measure_space_def"measure_integration/" )set type-eq-decl nil sets nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil measure_space_def"measure_integration/" )"set[T]" nat_indexed_sets "sets_aux/" )"(partial_order?[set[T]])" nil )"measurable_set[real, cal_M]" lebesgue_def nil )"complete_sigma_finite[real, cal_M]" nil )nil measure_def"measure_integration/" )"bool" measure_def"measure_integration/" )nil extended_nnreal"extended_nnreal/" )nil real_types nil )"set[T]" indexed_sets nil )nil measure_props "measure_integration/" )"set" sets nil )"bool" sets nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" reals nil )"[T, T -> boolean]" equalities nil )"bool" sets nil )"set[R]" function_image nil )"bool" extended_nnreal "extended_nnreal/" )"bool" measure_props "measure_integration/" )nil defined_types nil )nil naturalnumbers nil )nil lebesgue_defnil )nil nat_indexed_sets "sets_aux/" )nil nat_indexed_sets "sets_aux/" )"int" integers nil )"posint" nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil measure_space_def"measure_integration/" )"posint" nil ))nil ))nil 3475937691"" (skosimp)"" (lemma "measurable_IUnion" ("SS" "I!1" ))"" (expand "measurable_set?" ) (("" (propax) nil nil )) nil ))nil ))nil )"sigma_algebra" lebesgue_def nil )nil subset_algebra_def"measure_integration/" )"bool" subset_algebra_def"measure_integration/" )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 real_topology"metric_space/" )"bool" real_topology"metric_space/" )nil sequences nil )nil measure_space_def"measure_integration/" )"bool" measure_space_def"measure_integration/" )set type-eq-decl nil sets nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil measure_space_def"measure_integration/" ))nil ))nil 3475937691"" (skosimp)"" (typepred "E!1" )"" (expand "measurable_set?" ) (("" (assert ) nil nil )) nil ))nil ))nil )"bool" measure_props "measure_integration/" )"complete_sigma_finite[real, cal_M]" nil )nil measure_def"measure_integration/" )"bool" measure_def"measure_integration/" )nil extended_nnreal"extended_nnreal/" )nil real_types nil )"bool" reals nil )nil measure_space_def"measure_integration/" )"bool" measure_space_def"measure_integration/" )"sigma_algebra" lebesgue_def nil )nil subset_algebra_def"measure_integration/" )"bool" subset_algebra_def"measure_integration/" )nil sets nil )nil defined_types nil )set type-eq-decl nil sets 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 )"(partial_order?[set[T]])" nil )"measurable_set[real, cal_M]" lebesgue_def nil ))nil ))nil 3475946203"" (skosimp)"" (typepred "E!1" )"" (expand "mu_fin?" )"" (expand "mu" )"" (name "MU_E" "lambda_(E!1)" )"" (replace -1)"" (expand "lambda_" -1)"" (expand "lebesgue_measure" -1)"" (expand "induced_measure" -1)"" (expand "restrict" )"" (expand "lebesgue_outer_measure" )"" (expand "x_inf" )"" (lift-if -1)"" (assert )"" "" "" case "nonempty?({z_1: real | AND AND x`1 AND x`2 = z_1})") "1" case "bounded_below?({z_1: real | AND AND x`1 AND x`2 = z_1})") "1" "glb({z_1: real | AND AND x`1 AND x`2 = z_1})") "1" "GLB" "glb({z_1: real | AND AND x`1 AND x`2 = z_1})") "1" "1" replace -3 * rl)"1" assert )"1" "1" expand "greatest_lower_bound?" )"1" "1" expand "lower_bound?" )"1" "GLB+r!1/2" )"1" assert )"1" "1" "s!1" )"1" "1" "1" case "x!2`2<r!1 / 2 + GLB" )"1" "1" "I!1" )"1" assert )"1" case "x_le(lambda_(IUnion(I!1)), x_sum(lambda_ o I!1))" )"1" "x_sum_le" "S" "lambda_ o I!1" "T" "x_length o I!1" ))"1" "1" expand "x_le" "1" "1" assert )"1" "1" assert )"1" "1" assert )"1" "increasing_IUnion" "A" "I!1" ))"1" "1" case "forall n: IUnion(n, I!1)=B!1(n)" )"1" case "forall n: measurable_set?(B!1(n))" )"1" replace "1" "(LAMBDA n: lambda_(IUnion(n, I!1))`2)=LAMBDA n: lambda_(B!1(n))`2" )"1" "1" "m_increasing_convergence" "E" "B!1" ))"1" assert )"1" expand "x_converges?" )"1" "1" "LIMIT" "lambda_(IUnion(B!1))`2" )"1" expand "o " )"1" "FF" "(LAMBDA (i:nat): lambda_(B!1(i))`2)" )"1" "convergence_sequences.limit_lemma" "v" "FF" ))"1" replace "1" "1" expand "convergence" )"1" rewrite "metric_convergence_def" )"1" expand "metric_converges_to" )"1" "1" "r!2" )"1" "1" "n!1" )"1" "1" "i!1" )"1" assert )"1" expand "ball" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "measurable_set?" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil )"2" "2" "1" "x!3" )"1" replace "1" nil nil ))nil ))nil )"2" expand "measurable_set?" )"2" nil nil ))nil )"3" "3" "n!1" )"3" "n!1" )"3" expand "measurable_set?" )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" expand "measurable_set?" )"3" nil nil ))nil )"4" expand "measurable_set?" )"4" "4" "n!1" )"4" "n!1" )"4" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "n" )"1" "I!1(0)" )"1" "bounded_open_interval_is_measurable" )"1" "I!1(0)" )"1" assert )nil nil ))nil ))nil ))nil )"2" "2" "j!1" )"2" replace "2" rewrite "measurable_union" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "n" )"1" rewrite "IUnion_0_def" )"1" assert )nil nil ))nil )"2" "2" rewrite "IUnion_n_def" )"2" "j!1" )"2" replace "2" replace "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 "o " )"2" expand "lambda_" )"2" expand "lebesgue_measure" )"2" expand "induced_measure" )"2" expand "restrict" )"2" "lebesgue_outer_measure_le_length" "b" "I!1(i!1)" ))"1" nil nil )"2" "I!1(i!1)" )"2" expand "bounded_open_interval?" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "lambda_" )"2" expand "lebesgue_measure" )"2" expand "induced_measure" )"2" expand "restrict" )"2" expand "o " )"2" "lebesgue_outer_measure" )"2" expand "outer_measure?" )"2" "2" expand "om_countably_subadditive?" )"2" "I!1" )"2" expand "o " )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "I!1(x1!1)" )"3" "bounded_open_interval_is_measurable" "x" "I!1(x1!1)" ))"3" expand "measurable_set?" )"3" nil nil ))nil ))nil ))nil ))nil )"4" "measurable_IUnion" "SS" "I!1" ))"4" expand "measurable_set?" )"4" nil nil ))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 )"2" (assert ) nil nil ))nil )"2" "2" expand "bounded_below?" )"2" "0" )"2" expand "lower_bound?" )"2" "2" "s!1" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (propax) nil nil ))nil )"2" "2" expand "nonempty?" )"2" expand "empty?" )"2" expand "member" )"2" "x!1`2" )"2" "x!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "3" "I!1(x1!1)" )"3" expand "bounded_open_interval?" )"3" expand "bounded_interval?" )"3" (flatten) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" measure_props "measure_integration/" )"complete_sigma_finite[real, cal_M]" nil )nil measure_def"measure_integration/" )"bool" measure_def"measure_integration/" )nil extended_nnreal"extended_nnreal/" )nil real_types nil )"bool" reals nil )nil measure_space_def"measure_integration/" )"bool" measure_space_def"measure_integration/" )"sigma_algebra" lebesgue_def nil )nil subset_algebra_def"measure_integration/" )"bool" subset_algebra_def"measure_integration/" )nil sets nil )nil defined_types nil )set type-eq-decl nil sets 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 )"nnreal" measure_props "measure_integration/" )"complete_sigma_finite[real, lebesgue_measurable]" nil )"R" restrict nil )"extended_nnreal" extended_nnreal"extended_nnreal/" )"bool" sets nil )"bool" bounded_real_defs nil )"real" reals nil )nil real_types nil )"bool" reals nil )nil real_types 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 )nil nat_indexed_sets "sets_aux/" )"set[T]" nat_indexed_sets "sets_aux/" )"int" integers nil )"odd_int" integersnil )"posint" nil )nil measure_space_def"measure_integration/" )nil lebesgue_defnil )nil naturalnumbers nil )nil defined_types nil )"sequence[bounded_open_interval]" nil )"sequence[set[real]]" lebesgue_def nil )nil convergence_sequences "analysis/" )"bool" convergence_sequences "analysis/" )"[numfield, numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )nil metric_space"metric_space/" )"metric_open[real, (LAMBDA (x, y: real): abs(x - y))]" "metric_space/" )"(total_order?[real])" nil )"bool" sets nil )"set[T]" metric_space_def "metric_space/" )"bool" metric_space_def"metric_space/" )"bool" convergence_sequences "analysis/" )"real" reals nil )"bool" extended_nnreal "extended_nnreal/" )nil measure_props"measure_integration/" )nil nat_indexed_sets "sets_aux/" )nil nat_indexed_sets "sets_aux/" )"posint" nil )"(total_order?[real])" nil )nil nil )"bool" real_topology "metric_space/" )nil real_topology"metric_space/" )nil extended_nnreal "extended_nnreal/" )"bool" outer_measure_def"measure_integration/" )nil outer_measure_def"measure_integration/" )"bool" outer_measure_def"measure_integration/" )nil measure_space_def"measure_integration/" )"(strict_total_order?[real])" real_props nil )"(partial_order?[set[T]])" nil )"measurable_set[real, cal_M]" lebesgue_def nil )"posreal" nil )"bool" bounded_real_defs nil )"{x | greatest_lower_bound?(x, SB)}" nil )"bool" bounded_real_defs nil )"bool" sets nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )"bool" real_topology"metric_space/" )nil real_topology"metric_space/" )nil sequences nil )"bool" extended_nnreal "extended_nnreal/" )"extended_nnreal" extended_nnreal"extended_nnreal/" )"bool" real_topology "metric_space/" )nil real_topology "metric_space/" )"T3" function_props nil )"extended_nnreal" real_lebesgue_scaf nil )"bool" sets nil )"set[T]" indexed_sets nil )"outer_measure" nil )"complete_measure" outer_measure_props"measure_integration/" )"[T, T -> boolean]" equalities nil ))
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.310Bemerkung:
(vorverarbeitet am 2026-05-01)
¤ *© Formatika GbR, Deutschland
2026-05-26
