intervalIntegrable — Mathlib

English

If u is continuous on a set that contains the interval uIcc[a,b], then u is interval integrable on [a,b].

Русский

Если u непрерывна на множестве, содержащем uIcc[a,b], то u интервално интегрируема на [a,b].

LaTeX

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

Lean4

/-- A continuous function on `ℝ` is `IntervalIntegrable` with respect to any locally finite measure
`ν` on ℝ. -/
theorem intervalIntegrable {u : ℝ → E} (hu : Continuous u) (a b : ℝ) : IntervalIntegrable u μ a b :=
  hu.continuousOn.intervalIntegrable

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