|
(riemann_link
(bounded_on_def_TCC1 0
(bounded_on_def_TCC1-1 nil 3451819861
("" (skosimp) (("" (assert) nil nil)) nil)
((real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil))
nil))
(bounded_on_def 0
(bounded_on_def-1 nil 3451803010
("" (skosimp)
(("" (split)
(("1" (flatten)
(("1" (expand "zeroed_bounded?")
(("1" (split)
(("1" (expand "bounded_on?")
(("1" (skosimp)
(("1" (expand "bounded?")
(("1" (inst + "B!1")
(("1" (skosimp)
(("1" (expand "*")
(("1" (expand "phi")
(("1" (expand "member")
(("1"
(case-replace "closed(a!1, b!1)(x!1)")
(("1"
(inst - "x!1")
(("1" (grind) nil nil)
("2"
(hide 2)
(("2" (grind) nil nil))
nil))
nil)
("2"
(assert)
(("2"
(rewrite "zero_times1")
(("2"
(expand "abs" 2)
(("2"
(typepred "b!1")
(("2"
(inst - "(a!1+b!1)/2")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (typepred "b!1")
(("2" (inst - "(a!1+b!1)/2")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide -1)
(("2" (expand "zeroed?")
(("2" (skosimp) (("2" (grind) nil nil)) nil)) nil))
nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (expand "zeroed_bounded?")
(("2" (flatten)
(("2" (expand "bounded_on?")
(("2" (expand "bounded?")
(("2" (skosimp)
(("2" (inst + "c!1")
(("2" (skosimp)
(("2" (typepred "x!1")
(("2" (inst - "x!1")
(("2" (hide -4) (("2" (grind) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((zeroed_bounded? const-decl "bool" riemann_scaf nil)
(sigma_algebra? const-decl "bool" subset_algebra_def
"measure_integration/")
(sigma_algebra nonempty-type-eq-decl nil subset_algebra_def
"measure_integration/")
(cal_M const-decl "sigma_algebra" lebesgue_def nil)
(zeroed? const-decl "bool" riemann_scaf nil)
(bounded_on? const-decl "bool" integral_bounded "analysis/")
(bounded? const-decl "bool" sup_norm "measure_integration/")
(phi const-decl "nat" measure_space "measure_integration/")
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(<= const-decl "bool" reals nil) (set type-eq-decl nil sets nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(setof type-eq-decl nil defined_types nil)
(setofsets type-eq-decl nil sets nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(metric_induced_topology const-decl "setofsets[T]" metric_space_def
"metric_space/")
(closed? const-decl "bool" topology "topology/")
(closed nonempty-type-eq-decl nil topology "topology/")
(closed_ball const-decl "closed" real_topology "metric_space/")
(closed_interval nonempty-type-eq-decl nil real_topology
"metric_space/")
(closed const-decl "closed_interval" real_topology "metric_space/")
(< const-decl "bool" reals nil)
(minus_real_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(closed_is_measurable application-judgement "measurable_set"
lebesgue_def nil)
(closed_interval type-eq-decl nil intervals_real "reals/")
(b!1 skolem-const-decl "{x | a!1 < x}" riemann_link nil)
(x!1 skolem-const-decl "real" riemann_link nil)
(a!1 skolem-const-decl "real" riemann_link nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(/= const-decl "boolean" notequal nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(abs_0 formula-decl nil abs_lems "reals/")
(member const-decl "bool" sets nil)
(* const-decl "[T -> real]" real_fun_ops "reals/")
(real_times_real_is_real application-judgement "real" reals nil)
(nnreal type-eq-decl nil real_types nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(B!1 skolem-const-decl "real" riemann_link nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil))
shostak))
(riemann_integrable_def 0
(riemann_integrable_def-1 nil 3451801150
("" (skosimp)
(("" (split)
(("1" (flatten)
(("1" (case-replace "bounded_on?(a!1, b!1, f!1)")
(("1" (expand "<=")
(("1" (split)
(("1" (rewrite "bounded_on_def")
(("1" (rewrite "ae_continuous_def")
(("1"
(case "Integrable?(a!1, b!1, phi(closed(a!1, b!1)) * f!1)")
(("1"
(lemma
"Integrable_implies_ae_continuity[a!1,b!1]"
("f" "phi(closed(a!1, b!1)) * f!1"))
(("1" (assert) nil nil) ("2" (propax) nil nil)
("3" (propax) nil nil))
nil)
("2" (hide -2 2)
(("2" (expand "Integrable?")
(("2" (assert)
(("2"
(lemma "integral_restrict_eq"
("a" "a!1" "b" "b!1" "f" "f!1" "g"
"phi(closed(a!1, b!1)) * f!1"))
(("2" (assert)
(("2"
(hide -2 2)
(("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide -2 -3)
(("2" (expand "ae_continuous?")
(("2"
(case-replace
"{x | a!1 < x AND x < b!1 AND NOT continuous_at?(f!1, x)}=emptyset[real]")
(("1" (rewrite "null_emptyset") nil nil)
("2" (hide 2)
(("2" (apply-extensionality :hide? t)
(("2" (expand "emptyset")
(("2" (flatten) (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (expand "Integrable?")
(("2" (expand "<=" -2)
(("2" (split -2)
(("1" (assert)
(("1"
(lemma "integrable_bounded"
("a" "a!1" "b" "b!1" "f" "f!1"))
(("1" (assert) nil nil)) nil))
nil)
("2" (hide -2)
(("2" (expand "bounded_on?")
(("2" (inst + "abs(f!1(a!1))")
(("2" (skosimp) (("2" (ground) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (expand "<=" -3)
(("2" (split)
(("1" (rewrite "bounded_on_def")
(("1" (rewrite "ae_continuous_def")
(("1"
(lemma "ae_continuity_implies_Integrable[a!1,b!1]"
("f" "phi(closed(a!1, b!1)) * f!1"))
(("1" (assert)
(("1" (expand "Integrable?")
(("1"
(lemma "integral_restrict_eq"
("a" "a!1" "b" "b!1" "f"
"phi(closed(a!1, b!1)) * f!1" "g" "f!1"))
(("1" (assert)
(("1" (hide-all-but (-2 1))
(("1" (skosimp) (("1" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (propax) nil nil) ("3" (propax) nil nil))
nil))
nil))
nil)
("2" (expand "Integrable?") (("2" (flatten) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
((number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(bounded_on? const-decl "bool" integral_bounded "analysis/")
(ae_continuous_def formula-decl nil ae_continuous_def nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(member const-decl "bool" sets nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(integral_restrict_eq formula-decl nil integral_def "analysis/")
(Integrable_implies_ae_continuity formula-decl nil riemann_scaf
nil)
(zeroed_bounded? const-decl "bool" riemann_scaf nil)
(bounded nonempty-type-eq-decl nil riemann_scaf nil)
(Integrable? const-decl "bool" integral_def "analysis/")
(* const-decl "[T -> real]" real_fun_ops "reals/")
(set type-eq-decl nil sets nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(setof type-eq-decl nil defined_types nil)
(setofsets type-eq-decl nil sets nil)
(sigma_algebra? const-decl "bool" subset_algebra_def
"measure_integration/")
(sigma_algebra nonempty-type-eq-decl nil subset_algebra_def
"measure_integration/")
(cal_M const-decl "sigma_algebra" lebesgue_def nil)
(phi const-decl "nat" measure_space "measure_integration/")
(nnreal type-eq-decl nil real_types nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(metric_induced_topology const-decl "setofsets[T]" metric_space_def
"metric_space/")
(closed? const-decl "bool" topology "topology/")
(closed nonempty-type-eq-decl nil topology "topology/")
(closed_ball const-decl "closed" real_topology "metric_space/")
(closed_interval nonempty-type-eq-decl nil real_topology
"metric_space/")
(closed const-decl "closed_interval" real_topology "metric_space/")
(closed_is_measurable application-judgement "measurable_set"
lebesgue_def nil)
(< const-decl "bool" reals nil)
(bounded_on_def formula-decl nil riemann_link nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(ae_continuous? const-decl "bool" ae_continuous_def nil)
(lambda_ const-decl "complete_sigma_finite[real, cal_M]"
lebesgue_def nil)
(complete_sigma_finite type-eq-decl nil measure_def
"measure_integration/")
(complete_sigma_finite? const-decl "bool" measure_def
"measure_integration/")
(extended_nnreal nonempty-type-eq-decl nil extended_nnreal
"extended_nnreal/")
(null_emptyset judgement-tcc nil measure_theory
"measure_integration/")
(finite_emptyset name-judgement "finite_set" finite_sets nil)
(finite_emptyset name-judgement "finite_set[T]" sigma_countable
"sigma_set/")
(finite_emptyset name-judgement "finite_set[T]" bounded_nats
"orders/")
(finite_emptyset name-judgement "finite_set[T]" step_fun_props
"analysis/")
(finite_emptyset name-judgement "finite_set[T]" countable_props
"sets_aux/")
(finite_emptyset name-judgement "finite_set[T]" countable_setofsets
"sets_aux/")
(emptyset_is_compact name-judgement
"compact[real, (metric_induced_topology)]" convergence_aux
"metric_space/")
(emptyset_is_clopen name-judgement
"clopen[real, (metric_induced_topology)]" convergence_aux
"metric_space/")
(finite_emptyset name-judgement "finite_set[real]" integral_def
"analysis/")
(subset_algebra_emptyset name-judgement "(cal_M)" lebesgue_def nil)
(outer_negligible_emptyset name-judgement
"outer_negligible[real, lebesgue_outer_measure]"
real_lebesgue_scaf nil)
(subset_algebra_emptyset name-judgement "(induced_sigma_algebra)"
real_lebesgue_scaf nil)
(subset_algebra_emptyset name-judgement "(lebesgue_measurable)"
real_lebesgue_scaf nil)
(metric_space_is_hausdorff name-judgement "hausdorff[T]"
real_continuity "metric_space/")
(metric_space_is_hausdorff? name-judgement "(hausdorff?)"
real_continuity "metric_space/")
(metric_space_is_hausdorff? name-judgement "(hausdorff?)"
convergence_aux "metric_space/")
(metric_space_is_hausdorff name-judgement "hausdorff[real]"
convergence_aux "metric_space/")
(metric_induced_topology_is_second_countable name-judgement
"second_countable" real_topology "metric_space/")
(continuous_at? const-decl "bool" continuity_def "topology/")
(emptyset const-decl "set" sets nil)
(<= const-decl "bool" reals nil)
(integrable_bounded formula-decl nil integral_bounded "analysis/")
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(ae_continuity_implies_Integrable formula-decl nil riemann_scaf
nil)
(real_times_real_is_real application-judgement "real" reals nil))
shostak))
(riemann_lebesgue_integrable 0
(riemann_lebesgue_integrable-1 nil 3432041373
("" (skosimp)
(("" (rewrite "riemann_integrable_def")
(("" (flatten)
(("" (rewrite "ae_continuous_def")
(("" (expand "<=" -1)
(("" (split)
(("1" (rewrite "bounded_on_def")
(("1"
(lemma "ae_continuity_implies_integrable[a!1,b!1]"
("f" "phi(closed(a!1, b!1)) * f!1"))
(("1" (assert)
(("1" (expand "integrable?" 1)
(("1" (propax) nil nil)) nil))
nil)
("2" (propax) nil nil) ("3" (propax) nil nil))
nil))
nil)
("2" (expand "integrable?")
(("2" (replace -1 * rl)
(("2" (hide -1 -2 -3)
(("2" (lemma "integrable_singleton" ("x" "a!1"))
(("2"
(lemma "integrable_scal"
("c" "f!1(a!1)" "f"
"phi(singleton[real](a!1))"))
(("1"
(case-replace
"*[real](f!1(a!1), phi(singleton[real](a!1)))=phi(closed(a!1, a!1)) * f!1")
(("1" (hide-all-but 1)
(("1" (apply-extensionality :hide? t)
(("1" (grind) nil nil)) nil))
nil))
nil)
("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((riemann_integrable_def formula-decl nil riemann_link nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(ae_continuous_def formula-decl nil ae_continuous_def nil)
(closed_is_measurable application-judgement "measurable_set"
lebesgue_def nil)
(closed const-decl "closed_interval" real_topology "metric_space/")
(closed_interval nonempty-type-eq-decl nil real_topology
"metric_space/")
(closed_ball const-decl "closed" real_topology "metric_space/")
(closed nonempty-type-eq-decl nil topology "topology/")
(closed? const-decl "bool" topology "topology/")
(metric_induced_topology const-decl "setofsets[T]" metric_space_def
"metric_space/")
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(nnreal type-eq-decl nil real_types nil)
(phi const-decl "nat" measure_space "measure_integration/")
(cal_M const-decl "sigma_algebra" lebesgue_def nil)
(sigma_algebra nonempty-type-eq-decl nil subset_algebra_def
"measure_integration/")
(sigma_algebra? const-decl "bool" subset_algebra_def
"measure_integration/")
(setofsets type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(set type-eq-decl nil sets nil)
(* const-decl "[T -> real]" real_fun_ops "reals/")
(bounded nonempty-type-eq-decl nil riemann_scaf nil)
(zeroed_bounded? const-decl "bool" riemann_scaf nil)
(ae_continuity_implies_integrable formula-decl nil riemann_scaf
nil)
(integrable? const-decl "bool" indefinite_integral
"measure_integration/")
(bounded_on_def formula-decl nil riemann_link nil)
(bool nonempty-type-eq-decl nil booleans nil)
(< const-decl "bool" reals nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(integrable_singleton formula-decl nil lebesgue_def nil)
(* const-decl "[T -> real]" real_fun_ops "reals/")
(member const-decl "bool" sets nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(singleton_is_null application-judgement "null_set" lebesgue_def
nil)
(nonempty_singleton_finite application-judgement
"non_empty_finite_set[real]" integral_def "analysis/")
(singleton_is_compact application-judgement
"compact[real, (metric_induced_topology)]" convergence_aux
"metric_space/")
(singleton_is_closed application-judgement
"closed[real, (metric_induced_topology)]" convergence_aux
"metric_space/")
(integrable_scal judgement-tcc nil integral "measure_integration/")
(integrable? const-decl "bool" integral "measure_integration/")
(integrable nonempty-type-eq-decl nil integral
"measure_integration/")
(singleton? const-decl "bool" sets nil)
(singleton const-decl "(singleton?)" sets nil)
(extended_nnreal nonempty-type-eq-decl nil extended_nnreal
"extended_nnreal/")
(complete_sigma_finite? const-decl "bool" measure_def
"measure_integration/")
(complete_sigma_finite type-eq-decl nil measure_def
"measure_integration/")
(lambda_ const-decl "complete_sigma_finite[real, cal_M]"
lebesgue_def nil)
(<= const-decl "bool" reals nil))
shostak))
(riemann_lebesgue_integral_TCC1 0
(riemann_lebesgue_integral_TCC1-1 nil 3431800007
("" (skosimp)
((""
(lemma "riemann_lebesgue_integrable"
("a" "a!1" "b" "b!1" "f" "f!1"))
(("" (assert) nil nil)) nil))
nil)
((real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(riemann_lebesgue_integrable formula-decl nil riemann_link nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(closed_is_measurable application-judgement "measurable_set"
lebesgue_def nil))
nil))
(riemann_lebesgue_integral 0
(riemann_lebesgue_integral-1 nil 3451826406
("" (skosimp)
((""
(lemma "riemann_integrable_def" ("a" "a!1" "b" "b!1" "f" "f!1"))
(("" (assert)
(("" (flatten)
(("" (expand "integral")
(("" (rewrite "ae_continuous_def")
(("" (expand "<=" -3)
(("" (split)
(("1" (rewrite "bounded_on_def")
(("1"
(lemma "ae_continuity_implies_integrals[a!1,b!1]"
("f" "phi(closed(a!1, b!1)) * f!1"))
(("1" (assert)
(("1" (replace -1)
(("1" (hide -1 -3 -4)
(("1" (expand "Integrable?")
(("1"
(expand "Integral")
(("1"
(lemma
"integral_restrict_eq"
("a"
"a!1"
"b"
"b!1"
"f"
"f!1"
"g"
"phi(closed(a!1, b!1)) * f!1"))
(("1"
(assert)
(("1"
(hide -2 2)
(("1" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (propax) nil nil) ("3" (propax) nil nil))
nil))
nil)
("2" (expand "Integral")
(("2" (assert)
(("2" (replace -1 * rl)
(("2"
(lemma "integrable_singleton" ("x" "a!1"))
(("2"
(lemma "integrable_scal"
("c" "f!1(a!1)" "f"
"phi(singleton[real](a!1))"))
(("1" (hide -4 -5 -6)
(("1"
(lemma
"integral_singleton"
("x" "a!1"))
(("1"
(lemma
"integral_scal"
("c"
"f!1(a!1)"
"f"
"phi(singleton[real](a!1))"))
(("1"
(replace -2)
(("1"
(case-replace
"(*[real])(f!1(a!1),phi(singleton[real](a!1)))=(*[real])(phi(closed(a!1, a!1)),f!1)")
(("1" (assert) nil nil)
("2"
(hide-all-but 1)
(("2"
(apply-extensionality
:hide?
t)
(("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(riemann_integrable_def formula-decl nil riemann_link nil)
(ae_continuous_def formula-decl nil ae_continuous_def nil)
(closed const-decl "closed_interval" real_topology "metric_space/")
(closed_interval nonempty-type-eq-decl nil real_topology
"metric_space/")
(closed_ball const-decl "closed" real_topology "metric_space/")
(closed nonempty-type-eq-decl nil topology "topology/")
(closed? const-decl "bool" topology "topology/")
(metric_induced_topology const-decl "setofsets[T]" metric_space_def
"metric_space/")
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(nnreal type-eq-decl nil real_types nil)
(phi const-decl "nat" measure_space "measure_integration/")
(cal_M const-decl "sigma_algebra" lebesgue_def nil)
(sigma_algebra nonempty-type-eq-decl nil subset_algebra_def
"measure_integration/")
(sigma_algebra? const-decl "bool" subset_algebra_def
"measure_integration/")
(setofsets type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(set type-eq-decl nil sets nil)
(* const-decl "[T -> real]" real_fun_ops "reals/")
(bounded nonempty-type-eq-decl nil riemann_scaf nil)
(zeroed_bounded? const-decl "bool" riemann_scaf nil)
(ae_continuity_implies_integrals formula-decl nil riemann_scaf nil)
(Integrable? const-decl "bool" integral_def "analysis/")
(integral_restrict_eq formula-decl nil integral_def "analysis/")
(NOT const-decl "[bool -> bool]" booleans nil)
(member const-decl "bool" sets nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(Integral const-decl "real" integral_def "analysis/")
(bounded_on_def formula-decl nil riemann_link nil)
(bool nonempty-type-eq-decl nil booleans nil)
(< const-decl "bool" reals nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(integrable_singleton formula-decl nil lebesgue_def nil)
(integral_scal formula-decl nil integral "measure_integration/")
(* const-decl "[T -> real]" real_fun_ops "reals/")
(real_times_real_is_real application-judgement "real" reals nil)
(integral_singleton formula-decl nil lebesgue_def nil)
(singleton_is_null application-judgement "null_set" lebesgue_def
nil)
(nonempty_singleton_finite application-judgement
"non_empty_finite_set[real]" integral_def "analysis/")
(singleton_is_compact application-judgement
"compact[real, (metric_induced_topology)]" convergence_aux
"metric_space/")
(singleton_is_closed application-judgement
"closed[real, (metric_induced_topology)]" convergence_aux
"metric_space/")
(integrable_scal judgement-tcc nil integral "measure_integration/")
(integrable? const-decl "bool" integral "measure_integration/")
(integrable nonempty-type-eq-decl nil integral
"measure_integration/")
(singleton? const-decl "bool" sets nil)
(singleton const-decl "(singleton?)" sets nil)
(extended_nnreal nonempty-type-eq-decl nil extended_nnreal
"extended_nnreal/")
(complete_sigma_finite? const-decl "bool" measure_def
"measure_integration/")
(complete_sigma_finite type-eq-decl nil measure_def
"measure_integration/")
(lambda_ const-decl "complete_sigma_finite[real, cal_M]"
lebesgue_def nil)
(<= const-decl "bool" reals nil)
(integral const-decl "real" indefinite_integral
"measure_integration/")
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(closed_is_measurable application-judgement "measurable_set"
lebesgue_def nil))
shostak))
(bounded_ae_continuous_integrable 0
(bounded_ae_continuous_integrable-1 nil 3452433203
("" (skosimp)
((""
(lemma "riemann_integrable_def" ("f" "f!1" "a" "a!1" "b" "b!1"))
(("" (assert)
((""
(lemma "riemann_lebesgue_integrable"
("a" "a!1" "b" "b!1" "f" "f!1"))
(("" (assert) nil nil)) nil))
nil))
nil))
nil)
((real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(riemann_integrable_def formula-decl nil riemann_link nil)
(riemann_lebesgue_integrable formula-decl nil riemann_link nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(closed_is_measurable application-judgement "measurable_set"
lebesgue_def nil))
shostak))
(continuous_is_Integrable 0
(continuous_is_Integrable-1 nil 3452491862
("" (skosimp)
((""
(lemma "continuous_integrable" ("a" "a!1" "b" "b!1" "f" "f!1"))
(("" (expand "Integrable?")
(("" (assert)
(("" (skosimp)
(("" (expand "<=" -2)
(("" (replace 1)
(("" (replace -2)
(("" (assert)
(("" (hide-all-but (-1 -2 1))
(("" (skosimp)
(("" (typepred "x!1")
((""
(rewrite "continuous_iff_continuous_at?")
(("" (expand "continuous?")
(("" (inst - "x!1") nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(continuous_integrable formula-decl nil integral_cont "analysis/")
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(<= const-decl "bool" reals nil)
(closed_interval type-eq-decl nil intervals_real "reals/")
(AND const-decl "[bool, bool -> bool]" booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(continuous? const-decl "bool" continuity_def "topology/")
(real_minus_real_is_real application-judgement "real" reals nil)
(continuous_iff_continuous_at? formula-decl nil continuity_link
"metric_space/")
(Integrable? const-decl "bool" integral_def "analysis/"))
shostak))
(continuous_is_integrable 0
(continuous_is_integrable-1 nil 3476118188
("" (skosimp)
((""
(lemma "continuous_is_Integrable"
("a" "a!1" "b" "b!1" "f" "f!1"))
(("" (assert)
((""
(lemma "riemann_lebesgue_integrable"
("a" "a!1" "b" "b!1" "f" "f!1"))
(("" (assert) nil nil)) nil))
nil))
nil))
nil)
((real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(continuous_is_Integrable formula-decl nil riemann_link nil)
(riemann_lebesgue_integrable formula-decl nil riemann_link nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(closed_is_measurable application-judgement "measurable_set"
lebesgue_def nil))
shostak))
(continuous_at_is_bounded 0
(continuous_at_is_bounded-1 nil 3452514139
("" (skosimp)
(("" (expand "<=" -1)
(("" (split)
(("1"
(lemma "continuous_integrable"
("a" "a!1" "b" "b!1" "f" "f!1"))
(("1" (assert)
(("1" (split -1)
(("1"
(lemma "riemann_integrable_def"
("a" "a!1" "b" "b!1" "f" "f!1"))
(("1" (assert)
(("1" (expand "Integrable?") (("1" (propax) nil nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (skosimp)
(("2" (inst - "x!1")
(("2" (assert)
(("2" (rewrite "continuous_iff_continuous_at?")
nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide -2)
(("2" (expand "bounded_on?")
(("2" (inst + "abs(f!1(a!1))") (("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
((<= const-decl "bool" reals nil) (>= const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bounded_on? const-decl "bool" integral_bounded "analysis/")
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(continuous_integrable formula-decl nil integral_cont "analysis/")
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(Integrable? const-decl "bool" integral_def "analysis/")
(riemann_integrable_def formula-decl nil riemann_link nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(continuous_iff_continuous_at? formula-decl nil continuity_link
"metric_space/")
(closed_interval type-eq-decl nil intervals_real "reals/")
(AND const-decl "[bool, bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
shostak)))
[ zur Elbe Produktseite wechseln0.150Quellennavigators
Analyse erneut starten
]
|
