|
|
|
|
SSL lebesgue_fundamental.prf
Interaktion und
PortierbarkeitLisp
|
|
(lebesgue_fundamental
(IMP_fundamental_theorem_TCC1 0
(IMP_fundamental_theorem_TCC1-1 nil 3452514920 ("" (assert) nil nil)
((real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil))
nil))
(IMP_fundamental_theorem_TCC2 0
(IMP_fundamental_theorem_TCC2-1 nil 3452514920
("" (expand "connected?")
(("" (skosimp*)
(("" (typepred "x!1")
(("" (typepred "y!1")
(("" (expand "closed")
(("" (expand "closed_ball") (("" (grind) nil nil)) nil))
nil))
nil))
nil))
nil))
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)
(minus_real_is_real application-judgement "real" reals nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(real nonempty-type-from-decl nil reals nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(<= const-decl "bool" reals nil) (set type-eq-decl nil sets nil)
(>= const-decl "bool" reals nil)
(nnreal type-eq-decl nil real_types 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/")
(a formal-const-decl "real" lebesgue_fundamental nil)
(< const-decl "bool" reals nil)
(b formal-const-decl "{x: real | a < x}" lebesgue_fundamental nil)
(connected? const-decl "bool" deriv_domain_def "analysis/"))
nil))
(IMP_fundamental_theorem_TCC3 0
(IMP_fundamental_theorem_TCC3-1 nil 3452514920
("" (expand "not_one_element?")
(("" (skosimp)
(("" (typepred "x!1")
(("" (case "x!1=a")
(("1" (inst + "b")
(("1" (assert) nil nil)
("2" (hide -2) (("2" (grind) nil nil)) nil))
nil)
("2" (inst + "a")
(("1" (assert) nil nil)
("2" (hide -1 2) (("2" (grind) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((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)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(closed_is_measurable application-judgement "measurable_set"
lebesgue_def nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(real nonempty-type-from-decl nil reals nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(<= const-decl "bool" reals nil) (set type-eq-decl nil sets nil)
(>= const-decl "bool" reals nil)
(nnreal type-eq-decl nil real_types 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/")
(a formal-const-decl "real" lebesgue_fundamental nil)
(< const-decl "bool" reals nil)
(b formal-const-decl "{x: real | a < x}" lebesgue_fundamental nil)
(not_one_element? const-decl "bool" deriv_domain_def "analysis/"))
nil))
(IMP_fundamental_theorem_TCC4 0
(IMP_fundamental_theorem_TCC4-1 nil 3452518094
("" (inst + "a") (("" (grind) nil nil)) 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_le_is_total_order name-judgement "(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)
(b formal-const-decl "{x: real | a < x}" lebesgue_fundamental nil)
(< const-decl "bool" reals nil)
(a formal-const-decl "real" lebesgue_fundamental 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)
(setofsets type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil) (set type-eq-decl nil sets nil)
(<= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(closed_is_measurable application-judgement "measurable_set"
lebesgue_def nil))
nil))
(IMP_restriction_integral_TCC1 0
(IMP_restriction_integral_TCC1-1 nil 3452523885
("" (skosimp*)
(("" (typepred "x!1")
(("" (typepred "y!1") (("" (grind) nil nil)) nil)) nil))
nil)
((b formal-const-decl "{x: real | a < x}" lebesgue_fundamental nil)
(< const-decl "bool" reals nil)
(a formal-const-decl "real" lebesgue_fundamental 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)
(setofsets type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil) (set type-eq-decl nil sets nil)
(<= const-decl "bool" reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(real nonempty-type-from-decl nil reals nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans 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_le_is_total_order name-judgement "(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)
(minus_real_is_real application-judgement "real" reals nil))
nil))
(IMP_restriction_integral_TCC2 0
(IMP_restriction_integral_TCC2-1 nil 3452523885
("" (skosimp) (("" (inst + "x!1+1") (("" (assert) nil nil)) nil))
nil)
nil nil))
(IMP_restriction_integral_TCC3 0
(IMP_restriction_integral_TCC3-2 nil 3477731956
("" (skosimp)
(("" (typepred "x!1")
(("" (case "x!1=a")
(("1" (inst + "b")
(("1" (assert) nil nil)
("2" (hide -2) (("2" (grind) nil nil)) nil))
nil)
("2" (inst + "a")
(("1" (assert) nil nil)
("2" (hide -1 2) (("2" (grind) nil nil)) nil))
nil))
nil))
nil))
nil)
((b formal-const-decl "{x: real | a < x}" lebesgue_fundamental nil)
(< const-decl "bool" reals nil)
(a formal-const-decl "real" lebesgue_fundamental 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)
(setofsets type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil) (set type-eq-decl nil sets nil)
(<= const-decl "bool" reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(real nonempty-type-from-decl nil reals nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(closed_is_measurable application-judgement "measurable_set"
lebesgue_def 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_le_is_total_order name-judgement "(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)
(minus_real_is_real application-judgement "real" reals nil))
nil)
(IMP_restriction_integral_TCC3-1 nil 3452523885
("" (skosimp) (("" (inst + "x!1") nil nil)) nil)
((set type-eq-decl nil sets nil)
(setofsets type-eq-decl nil sets 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/"))
nil))
(IMP_restriction_integral_TCC4 0
(IMP_restriction_integral_TCC4-1 nil 3477673281
("" (skosimp*) (("" (inst + "x!1+1") (("" (assert) nil nil)) nil))
nil)
((real_plus_real_is_real application-judgement "real" reals 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)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields
nil))
nil))
(IMP_restriction_integral_TCC5 0
(IMP_restriction_integral_TCC5-2 nil 3477731995
("" (skosimp*)
(("" (typepred "x!1") (("" (inst + "x!1") nil nil)) nil)) nil)
((b formal-const-decl "{x: real | a < x}" lebesgue_fundamental nil)
(< const-decl "bool" reals nil)
(a formal-const-decl "real" lebesgue_fundamental 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)
(setofsets type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil) (set type-eq-decl nil sets nil)
(<= const-decl "bool" reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(real nonempty-type-from-decl nil reals nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
nil)
(IMP_restriction_integral_TCC5-1 nil 3477673281
("" (assuming-tcc) nil nil) nil nil))
(F_TCC1 0
(F_TCC1-1 nil 3603447121
("" (lemma "deriv_domain") (("" (propax) nil nil)) nil)
((deriv_domain formula-decl nil fundamental_theorem "analysis/")
(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) (set type-eq-decl nil sets nil)
(>= const-decl "bool" reals nil)
(nnreal type-eq-decl nil real_types 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/")
(a formal-const-decl "real" lebesgue_fundamental nil)
(< const-decl "bool" reals nil)
(b formal-const-decl "{x: real | a < x}" lebesgue_fundamental nil))
nil))
(fundamental_lebesgue_TCC1 0
(fundamental_lebesgue_TCC1-1 nil 3452514920
("" (skosimp) (("" (hide -1 -2) (("" (grind) nil nil)) nil)) nil)
((minus_real_is_real application-judgement "real" reals nil)
(closed_ball const-decl "closed" real_topology "metric_space/")
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(closed const-decl "closed_interval" real_topology "metric_space/")
(closed_is_measurable application-judgement "measurable_set"
lebesgue_def 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_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_minus_real_is_real application-judgement "real" reals nil))
nil))
(fundamental_lebesgue_TCC2 0
(fundamental_lebesgue_TCC2-1 nil 3452514920
("" (skosimp) (("" (hide -1 -2) (("" (grind) nil nil)) nil)) nil)
((closed_ball const-decl "closed" real_topology "metric_space/")
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(closed const-decl "closed_interval" real_topology "metric_space/")
(closed_is_measurable application-judgement "measurable_set"
lebesgue_def 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_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_minus_real_is_real application-judgement "real" reals nil))
nil))
(fundamental_lebesgue 0
(fundamental_lebesgue-1 nil 3452515121
("" (skosimp*)
(("" (typepred "F!1")
(("" (typepred "f!1")
((""
(lemma "continuous_at_is_ae_continuous"
("a" "a" "b" "b" "f" "f!1"))
((""
(lemma "bounded_ae_continuous_integrable"
("a" "a" "b" "b" "f" "f!1"))
((""
(lemma "continuous_at_is_bounded"
("a" "a" "b" "b" "f" "f!1"))
(("" (assert)
(("" (assert)
((""
(case-replace
"(FORALL x: a <= x AND x <= b => continuous_at?(f!1, x))")
(("1" (split -4)
(("1" (assert)
(("1" (hide -5)
(("1"
(lemma "riemann_integrable_def"
("a" "a" "b" "b" "f" "f!1"))
(("1" (assert)
(("1"
(lemma
"fundamental3"
("F" "F!1" "f" "f!1" "a" "a" "b" "b"))
(("1"
(replace -8)
(("1"
(replace -7)
(("1"
(split -1)
(("1"
(flatten)
(("1"
(assert)
(("1"
(hide -1 -2)
(("1"
(expand "restrict")
(("1"
(lemma
"riemann_lebesgue_integral"
("a"
"a"
"b"
"b"
"f"
"f!1"))
(("1"
(assert)
(("1"
(replace -1 1 rl)
(("1"
(case-replace
"(LAMBDA (s_1: real): f!1(s_1)) = f!1")
(("1"
(lemma
"fundamental3[(closed(a, b))]"
("a"
"a"
"b"
"b"
"F"
"F!1"
"f"
"LAMBDA (s_1:(closed(a, b))): f!1(s_1)"))
(("1"
(replace -10)
(("1"
(replace
-9)
(("1"
(split)
(("1"
(flatten)
(("1"
(lemma
"restrict_Integral")
(("1"
(inst
-
"a"
"b"
"f!1")
(("1"
(assert)
nil
nil))
nil))
nil))
nil)
("2"
(hide-all-but
(1
-5))
(("2"
(expand
"continuous?")
(("2"
(skosimp)
(("2"
(inst
-
"x0!1")
(("2"
(typepred
"x0!1")
(("2"
(split)
(("1"
(rewrite
"metric_continuous_at_def")
(("1"
(expand
"continuous?")
(("1"
(expand
"metric_continuous_at?")
(("1"
(skosimp)
(("1"
(inst
-
"epsilon!1")
(("1"
(skosimp)
(("1"
(inst
+
"delta!1")
(("1"
(skosimp)
(("1"
(typepred
"x!1")
(("1"
(inst
-
"x!1")
(("1"
(split)
(("1"
(hide-all-but
(-1
1))
(("1"
(grind)
nil
nil))
nil)
("2"
(hide-all-but
(-3
1))
(("2"
(grind)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide
2)
(("2"
(grind)
nil
nil))
nil)
("3"
(hide
2)
(("3"
(grind)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(apply-extensionality
:hide?
t)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but (-3 1))
(("2"
(expand "restrict")
(("2"
(assert)
(("2"
(expand "continuous?")
(("2"
(skosimp)
(("2"
(inst - "x0!1")
(("2"
(typepred "x0!1")
(("2"
(split -2)
(("1"
(rewrite
"metric_continuous_at_def")
(("1"
(expand
"continuous?")
(("1"
(expand
"metric_continuous_at?")
(("1"
(skosimp)
(("1"
(inst
-
"epsilon!1")
(("1"
(skosimp)
(("1"
(inst
+
"delta!1")
(("1"
(skosimp)
(("1"
(inst
-
"x!1")
(("1"
(split)
(("1"
(hide-all-but
(-1
1))
(("1"
(grind)
nil
nil))
nil)
("2"
(hide-all-but
(-2
1))
(("2"
(grind)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(grind)
nil
nil))
nil)
("3"
(hide 2)
(("3"
(grind)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but (-1 1))
(("2" (skosimp)
(("2" (inst - "x!1") (("2" (assert) nil nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but (-4 1))
(("2" (expand "continuous_on?")
(("2" (skosimp)
(("2" (inst - "x!1")
(("2" (hide 2) (("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((deriv_fun type-eq-decl nil derivatives "analysis/")
(derivable? const-decl "bool" derivatives "analysis/")
(b formal-const-decl "{x: real | a < x}" lebesgue_fundamental nil)
(< const-decl "bool" reals nil)
(a formal-const-decl "real" lebesgue_fundamental 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)
(setofsets type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil) (set type-eq-decl nil sets nil)
(<= const-decl "bool" reals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(continuous_at_is_ae_continuous formula-decl nil ae_continuous_def
nil)
(continuous_at_is_bounded formula-decl nil riemann_link nil)
(x!1 skolem-const-decl "real" lebesgue_fundamental nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(restrict_Integral formula-decl nil restriction_integral nil)
(continuous? const-decl "bool" continuous_functions "analysis/")
(continuous? const-decl "bool" continuous_functions "analysis/")
(minus_real_is_real application-judgement "real" reals nil)
(member const-decl "bool" sets nil)
(ball const-decl "set[T]" metric_space_def "metric_space/")
(ball_is_metric_open application-judgement
"metric_open[real, (LAMBDA (x, y: real): abs(x - y))]"
convergence_aux "metric_space/")
(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)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(metric_continuous_at? const-decl "bool" metric_continuity
"metric_space/")
(metric_continuous_at_def formula-decl nil metric_continuity
"metric_space/")
(real_div_nzreal_is_real application-judgement "real" reals nil)
(riemann_lebesgue_integral formula-decl nil riemann_link nil)
(restrict const-decl "R" restrict nil)
(fundamental3 formula-decl nil fundamental_theorem "analysis/")
(riemann_integrable_def formula-decl nil riemann_link nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(continuous_at? const-decl "bool" continuity_def "topology/")
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(closed_is_measurable application-judgement "measurable_set"
lebesgue_def nil)
(bounded_ae_continuous_integrable formula-decl nil riemann_link
nil)
(continuous_on? const-decl "bool" continuous_on nil)
(continuous_on type-eq-decl nil continuous_on nil))
shostak))
(integration_by_parts_TCC1 0
(integration_by_parts_TCC1-1 nil 3476038809
("" (skosimp) (("" (hide-all-but 1) (("" (grind) nil nil)) nil))
nil)
((minus_real_is_real application-judgement "real" reals nil)
(closed_ball const-decl "closed" real_topology "metric_space/")
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(closed const-decl "closed_interval" real_topology "metric_space/")
(closed_is_measurable application-judgement "measurable_set"
lebesgue_def 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_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_minus_real_is_real application-judgement "real" reals nil))
nil))
(integration_by_parts_TCC2 0
(integration_by_parts_TCC2-1 nil 3476038809
("" (skosimp) (("" (hide-all-but 1) (("" (grind) nil nil)) nil))
nil)
((closed_ball const-decl "closed" real_topology "metric_space/")
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(closed const-decl "closed_interval" real_topology "metric_space/")
(closed_is_measurable application-judgement "measurable_set"
lebesgue_def 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_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_minus_real_is_real application-judgement "real" reals nil))
nil))
(integration_by_parts 0
(integration_by_parts-1 nil 3476040864
("" (skosimp)
(("" (name "H" "real_fun_ops.*(F!1,G!1)")
(("1" (lemma "prod_derivable_fun" ("f1" "F!1" "f2" "G!1"))
(("1" (split)
(("1" (lemma "deriv_prod_fun" ("ff1" "F!1" "ff2" "G!1"))
(("1" (lemma "fundamental_lebesgue" ("F" "H"))
(("1" (replace -4)
(("1" (replace -2)
(("1" (replace -5)
(("1" (replace -6)
(("1" (hide -4 -5 -6)
(("1" (hide -3 -2)
(("1" (expand "H" -)
(("1" (expand "*" - 3)
(("1"
(expand "*" - 4)
(("1"
(expand "restrict" -)
(("1"
(expand "*" - 1)
(("1"
(expand "+" - 1)
(("1"
(assert)
(("1"
(expand "*" - 1)
(("1"
(typepred "f!1")
(("1"
(typepred "g!1")
(("1"
(lemma
"derivable_cont_fun[(closed(a, b))]")
(("1"
(inst-cp - "F!1")
(("1"
(inst - "G!1")
(("1"
(assert)
(("1"
(name
"CE"
"lambda (f:[real->real]): lambda x: if x<a then f(a) elsif b<x then f(b) else f(x) endif")
(("1"
(hide -1)
(("1"
(case
"FORALL (f:[real->real]): (forall x: closed(a,b)(x) => continuous_at?(f,x)) => continuity_def.continuous?(CE(f))")
(("1"
(case
"FORALL (f:[real->real],x): closed(a, b)(x) => CE(f)(x) = f(x)")
(("1"
(name-replace
"FF"
"extend[real, (closed(a, b)), real, 0](F!1)")
(("1"
(name-replace
"GG"
"extend[real, (closed(a, b)), real, 0](G!1)")
(("1"
(inst-cp
-
"f!1")
(("1"
(inst-cp
-
"g!1")
(("1"
(split)
(("1"
(split)
(("1"
(inst-cp
-
"g!1"
"_")
(("1"
(inst-cp
-
"f!1"
"_")
(("1"
(hide
-6)
(("1"
(case
"continuity_def.continuous?(CE(GG)*CE(f!1))")
(("1"
(case
"continuity_def.continuous?(CE(FF)*CE(g!1))")
(("1"
(case
"continuity_def.continuous?((CE(FF)*CE(g!1)) + (CE(GG)*CE(f!1)))")
(("1"
(inst
-13
"(CE(FF) * CE(g!1)) + (CE(GG) * CE(f!1))")
(("1"
(split
-13)
(("1"
(flatten)
(("1"
(lemma
"continuous_is_integrable"
("a"
"a"
"b"
"b"
"f"
"CE(GG) * CE(f!1)"))
(("1"
(lemma
"continuous_is_integrable"
("a"
"a"
"b"
"b"
"f"
"CE(FF) * CE(g!1)"))
(("1"
(assert)
(("1"
(rewrite
"indefinite_add"
-4)
(("1"
(expand
"integral"
(1
-4))
(("1"
(expand
"integrable?"
(1
-1
-2))
(("1"
(expand
"*")
(("1"
(hide-all-but
(-1
-2
-3
-4
1))
(("1"
(expand
"phi")
(("1"
(expand
"member")
(("1"
(case-replace
"(LAMBDA (x_1: real):
IF closed(a, b)(x_1) THEN 1 ELSE 0 ENDIF *
(CE(FF)(x_1) * CE(g!1)(x_1)))=(LAMBDA (x_1: real):
IF closed(a, b)(x_1) THEN 1 ELSE 0 ENDIF *
(FF(x_1) * g!1(x_1)))")
(("1"
(replace
-2)
(("1"
(hide
-1)
(("1"
(case-replace
"(LAMBDA (x_1: real):
IF closed(a, b)(x_1) THEN 1 ELSE 0 ENDIF *
(CE(GG)(x_1) * CE(f!1)(x_1)))=(LAMBDA (x_1: real):
IF closed(a, b)(x_1) THEN 1 ELSE 0 ENDIF *
(GG(x_1) * f!1(x_1)))")
(("1"
(hide
-1)
(("1"
(replace
-2)
(("1"
(assert)
nil
nil))
nil))
nil)
("2"
(hide-all-but
1)
(("2"
(apply-extensionality
:hide?
t)
(("2"
(expand
"CE")
(("2"
(grind)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but
1)
(("2"
(apply-extensionality
:hide?
t)
(("2"
(expand
"CE")
(("2"
(grind)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but
1)
(("2"
(apply-extensionality
:hide?
t)
(("2"
(expand
"CE")
(("2"
(typepred
"x!1")
(("2"
(expand
"GG")
(("2"
(expand
"FF")
(("2"
(grind)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but
(-1
1))
(("2"
(expand
"continuous_on?")
(("2"
(skosimp)
(("2"
(expand
"continuous?")
(("2"
(inst
-
"x!1")
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but
(-1
-2
1))
(("2"
(rewrite
"metric_continuous_def")
(("2"
(rewrite
"metric_continuous_def")
(("2"
(rewrite
"metric_continuous_def")
(("2"
(rewrite
"sum_continuous")
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but
(1
-3
-8))
(("2"
(rewrite
"metric_continuous_def")
(("2"
(rewrite
"metric_continuous_def")
(("2"
(rewrite
"prod_continuous")
(("2"
(hide
2
-1)
(("2"
(expand
"continuous?")
(("2"
(expand
"metric_continuous?")
(("2"
(skosimp)
(("2"
(case
"closed(a,b)(x!1)")
(("1"
(inst
-
"x!1")
(("1"
(expand
"continuous?")
(("1"
(expand
"metric_continuous_at?")
(("1"
(skosimp)
(("1"
(inst
-
"epsilon!1")
(("1"
(skosimp)
(("1"
(inst
+
"delta!1")
(("1"
(expand
"ball")
(("1"
(expand
"member")
(("1"
(skosimp)
(("1"
(expand
"CE")
(("1"
(case
"closed(a,b)(x!2)")
(("1"
(inst
-
"x!2")
(("1"
(split
-4)
(("1"
(hide
-4)
(("1"
(expand
"FF")
(("1"
(grind)
nil
nil))
nil))
nil)
("2"
(hide
2
-1
-2)
(("2"
(grind)
nil
nil))
nil))
nil))
nil)
("2"
(case
"x!2<a")
(("1"
(inst
-
"a")
(("1"
(expand
"FF")
(("1"
(split
-4)
(("1"
(grind)
nil
nil)
("2"
(hide
3)
(("2"
(grind)
nil
nil))
nil))
nil))
nil)
("2"
(hide-all-but
1)
(("2"
(grind)
nil
nil))
nil))
nil)
("2"
(case
"b<x!2")
(("1"
(inst
-
"b")
(("1"
(split)
(("1"
(expand
"FF")
(("1"
(grind)
nil
nil))
nil)
("2"
(hide
4)
(("2"
(grind)
nil
nil))
nil))
nil)
("2"
(hide-all-but
1)
(("2"
(grind)
nil
nil))
nil))
nil)
("2"
(hide-all-but
(1
2
3))
(("2"
(grind)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide
-1)
(("2"
(expand
"metric_continuous_at?")
(("2"
(skosimp)
(("2"
(expand
"ball")
(("2"
(expand
"member")
(("2"
(expand
"CE")
(("2"
(case-replace
"x!1<a")
(("1"
(inst
+
"a-x!1")
(("1"
(skosimp)
(("1"
(expand
"FF")
(("1"
(grind)
nil
nil))
nil))
nil)
("2"
(assert)
nil
nil))
nil)
("2"
(case-replace
"b<x!1")
(("1"
(inst
+
"x!1-b")
(("1"
(expand
"FF")
(("1"
(grind)
nil
nil))
nil)
("2"
(assert)
nil
nil))
nil)
("2"
(hide
4)
(("2"
(grind)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but
(1
-1
-6))
(("2"
(rewrite
"metric_continuous_def")
(("2"
(rewrite
"metric_continuous_def")
(("2"
(rewrite
"prod_continuous")
(("2"
(hide
-1
2)
(("2"
(expand
"metric_continuous?")
(("2"
(skosimp)
(("2"
(expand
"continuous?")
(("2"
(expand
"metric_continuous_at?")
(("2"
(case
"closed(a,b)(x!1)")
(("1"
(inst
-
"x!1")
(("1"
(expand
"continuous?")
(("1"
(skosimp)
(("1"
(expand
"CE")
(("1"
(expand
"member")
(("1"
(expand
"ball")
(("1"
(inst
-
"epsilon!1")
(("1"
(skosimp)
(("1"
(inst
+
"delta!1")
(("1"
(skosimp)
(("1"
(case
"closed(a, b)(x!2)")
(("1"
(inst
-
"x!2")
(("1"
(assert)
(("1"
(split
-4)
(("1"
(expand
"GG")
(("1"
(grind)
nil
nil))
nil)
("2"
(hide
-1
-2
2)
(("2"
(grind)
nil
nil))
nil))
nil))
nil))
nil)
("2"
(case-replace
"x!2 < a")
(("1"
(expand
"GG")
(("1"
(inst
-
"a")
(("1"
(grind)
nil
nil)
("2"
(hide-all-but
1)
(("2"
(grind)
nil
nil))
nil))
nil))
nil)
("2"
(case-replace
"b < x!2")
(("1"
(inst
-
"b")
(("1"
(expand
"GG")
(("1"
(split
-4)
(("1"
(hide
-4)
(("1"
(grind)
nil
nil))
nil)
("2"
(hide
4)
(("2"
(grind)
nil
nil))
nil))
nil))
nil)
("2"
(hide-all-but
1)
(("2"
(grind)
nil
nil))
nil))
nil)
("2"
(hide-all-but
(1
2
3))
(("2"
(grind)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand
"member")
(("2"
(expand
"ball")
(("2"
(hide
-1)
(("2"
(case
"x!1<a")
(("1"
(skosimp)
(("1"
(inst
+
"a-x!1")
(("1"
(skosimp)
(("1"
(expand
"CE")
(("1"
(grind)
nil
nil))
nil))
nil)
("2"
(assert)
nil
nil))
nil))
nil)
("2"
(case
"b<x!1")
(("1"
(skosimp)
(("1"
(inst
+
"x!1-b")
(("1"
(expand
"CE")
(("1"
(grind)
nil
nil))
nil)
("2"
(assert)
nil
nil))
nil))
nil)
("2"
(hide
4)
(("2"
(grind)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but
(-7
1))
(("2"
(skosimp)
(("2"
(expand
"continuous_on?")
(("2"
(inst
-
"x!1")
nil
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but
(1
-6))
(("2"
(skosimp)
(("2"
(expand
"continuous_on?")
(("2"
(inst
-
"x!1")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but
1)
(("2"
(expand
"CE")
(("2"
(grind)
nil
nil))
nil))
nil))
nil)
("2"
(hide-all-but
1)
(("2"
(skosimp)
(("2"
(rewrite
"metric_continuous_def")
(("2"
(expand
"CE")
(("2"
(expand
"metric_continuous?")
(("2"
(skosimp)
(("2"
(expand
"metric_continuous_at?")
(("2"
(skosimp)
(("2"
(expand
"ball")
(("2"
(expand
"member")
(("2"
(case-replace
"x!1 < a")
(("1"
(hide
-2)
(("1"
(inst
+
"a-x!1")
(("1"
(skosimp)
(("1"
(grind)
nil
nil))
nil)
("2"
(assert)
nil
nil))
nil))
nil)
("2"
(case-replace
"b < x!1")
(("1"
(hide
-2
1)
(("1"
(inst
+
"x!1-b")
(("1"
(grind)
nil
nil)
("2"
(assert)
nil
nil))
nil))
nil)
("2"
(assert)
(("2"
(inst
-
"x!1")
(("2"
(split
-1)
(("1"
(rewrite
"metric_continuous_at_def")
(("1"
(expand
"metric_continuous_at?")
(("1"
(inst
-
"epsilon!1")
(("1"
(skosimp)
(("1"
(expand
"ball")
(("1"
(expand
"member")
(("1"
(inst
+
"delta!1")
(("1"
(skosimp)
(("1"
(case-replace
"x!2 < a")
(("1"
(inst
-
"a")
(("1"
(split)
(("1"
(propax)
nil
nil)
("2"
(hide
4)
(("2"
(grind)
nil
nil))
nil))
nil))
nil)
("2"
(case-replace
"b < x!2")
(("1"
(inst
-
"b")
(("1"
(split)
(("1"
(assert)
nil
nil)
("2"
(hide
5)
(("2"
(grind)
nil
nil))
nil))
nil))
nil)
("2"
(assert)
(("2"
(inst
-
"x!2")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide
4)
(("2"
(grind)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil) ("3" (assert) nil nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil)
((deriv_fun type-eq-decl nil derivatives "analysis/")
(derivable? const-decl "bool" derivatives "analysis/")
(* const-decl "[T -> real]" real_fun_ops "reals/")
(b formal-const-decl "{x: real | a < x}" lebesgue_fundamental nil)
(< const-decl "bool" reals nil)
(a formal-const-decl "real" lebesgue_fundamental 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)
(setofsets type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil) (set type-eq-decl nil sets nil)
(<= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(prod_fun_continuous application-judgement "continuous_fun[T]"
integral "analysis/")
(derivable_prod application-judgement "deriv_fun" derivatives
"analysis/")
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(fundamental_lebesgue formula-decl nil lebesgue_fundamental nil)
(real_times_real_is_real application-judgement "real" reals nil)
(restrict const-decl "R" restrict nil)
(+ const-decl "[T -> real]" real_fun_ops "reals/")
(x!1 skolem-const-decl "real" lebesgue_fundamental nil)
(metric_continuous_at_def formula-decl nil metric_continuity
"metric_space/")
(x!1 skolem-const-decl "real" lebesgue_fundamental nil)
(continuous? const-decl "bool" continuous_functions "analysis/")
(ball const-decl "set[T]" metric_space_def "metric_space/")
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(x!2 skolem-const-decl "real" lebesgue_fundamental nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(metric_continuous_at? const-decl "bool" metric_continuity
"metric_space/")
(x!1 skolem-const-decl "real" lebesgue_fundamental nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(continuous? const-decl "bool" continuous_functions "analysis/")
(prod_continuous judgement-tcc nil real_continuity "metric_space/")
(continuous_is_integrable formula-decl nil riemann_link nil)
(integral const-decl "real" indefinite_integral
"measure_integration/")
(phi const-decl "nat" measure_space "measure_integration/")
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(minus_real_is_real application-judgement "real" reals nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(member const-decl "bool" sets nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(indefinite_add formula-decl nil indefinite_integral
"measure_integration/")
(measurable_set? const-decl "bool" measure_space_def
"measure_integration/")
(measurable_set nonempty-type-eq-decl nil measure_space_def
"measure_integration/")
(integrable? const-decl "bool" indefinite_integral
"measure_integration/")
(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)
(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 "[numfield, numfield -> numfield]" number_fields nil)
(f!1 skolem-const-decl "continuous_on[(closed(a, b))]"
lebesgue_fundamental nil)
(GG skolem-const-decl "[real -> real]" lebesgue_fundamental nil)
(g!1 skolem-const-decl "continuous_on[(closed(a, b))]"
lebesgue_fundamental nil)
(FF skolem-const-decl "[real -> real]" lebesgue_fundamental nil)
(CE skolem-const-decl "[[real -> real] -> [real -> real]]"
lebesgue_fundamental nil)
(metric_continuous_def formula-decl nil metric_continuity
"metric_space/")
(sum_continuous judgement-tcc nil real_continuity "metric_space/")
(metric_continuous? const-decl "bool" metric_continuity
"metric_space/")
(metric_continuous type-eq-decl nil metric_continuity
"metric_space/")
(x!2 skolem-const-decl "real" lebesgue_fundamental nil)
(x!1 skolem-const-decl "real" lebesgue_fundamental nil)
(x!1 skolem-const-decl "real" lebesgue_fundamental nil)
(extend const-decl "R" extend nil)
(continuous? const-decl "bool" continuity_def "topology/")
(continuous_at? const-decl "bool" continuity_def "topology/")
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(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/")
(metric_space_is_hausdorff name-judgement "hausdorff[T]"
real_continuity "metric_space/")
(metric_space_is_hausdorff? name-judgement "(hausdorff?)"
real_continuity "metric_space/")
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(derivable_cont_fun formula-decl nil derivatives "analysis/")
(continuous_on type-eq-decl nil continuous_on nil)
(continuous_on? const-decl "bool" continuous_on nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(closed_is_measurable application-judgement "measurable_set"
lebesgue_def nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(H skolem-const-decl "deriv_fun[(closed(a, b))]"
lebesgue_fundamental nil)
(deriv_prod_fun formula-decl nil derivatives "analysis/")
(prod_derivable_fun formula-decl nil derivatives "analysis/"))
shostak)))
| Messung V0.5 in Prozent |
|---|
| | | |
¤ Dauer der Verarbeitung: 0.95 Sekunden
(vorverarbeitet am 2026-04-27)
¤
*© Formatika GbR, Deutschland
|
|
2026-05-26
|
|
|
|
|
