intervalIntegrable_of_Icc — Mathlib

English

If a function u is continuous on the closed interval Icc[a,b], then it is interval integrable on [a,b] with respect to μ.

Русский

Если функция u непрерывна на замкнутом интервале Icc[a,b], то она интервално интегрируема на [a,b].

LaTeX

$$ContinuousOn(u, Icc(a,b)) \\Rightarrow IntervalIntegrable(u, μ, a, b)$$

Lean4

theorem intervalIntegrable_of_Icc {u : ℝ → E} {a b : ℝ} (h : a ≤ b) (hu : ContinuousOn u (Icc a b)) :
    IntervalIntegrable u μ a b :=
  ContinuousOn.intervalIntegrable ((uIcc_of_le h).symm ▸ hu)

Похожие утверждения