intervalIntegrable_iff — Mathlib

English

Interval integrability on [a,b] is equivalent to ordinary integrability of f on the oriented interval Ι(a,b).

Русский

Интервальная интегрируемость по отрезку [a,b] эквивалентна обычной интегрируемости по ориентированному интервалу Ι(a,b).

LaTeX

$$$$\text{IntervalIntegrable}(f,μ,a,b) \iff \text{IntegrableOn}(f,Ι(a,b),μ).$$$$

Lean4

/-- A function is interval integrable with respect to a given measure `μ` on `a..b` if and
  only if it is integrable on `uIoc a b` with respect to `μ`. This is an equivalent
  definition of `IntervalIntegrable`. -/
theorem intervalIntegrable_iff : IntervalIntegrable f μ a b ↔ IntegrableOn f (Ι a b) μ := by
  rw [uIoc_eq_union, integrableOn_union, IntervalIntegrable]

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