intervalIntegrable_iff_integrableOn_Ioc_of_le

English

If f is interval integrable on [a,b], then the integral over the interval is finite (under finiteness conditions on μ).

Русский

Если f интервально интегрируема на [a,b], то интеграл по интервалу конечен (при конечности меры μ).

LaTeX

$$$$\text{IntervalIntegrable}(f, μ, a, b) \implies \int_a^b f \,dμ < \infty.$$$$

Lean4

theorem intervalIntegrable_iff_integrableOn_Ioc_of_le (hab : a ≤ b) :
    IntervalIntegrable f μ a b ↔ IntegrableOn f (Ioc a b) μ := by rw [intervalIntegrable_iff, uIoc_of_le hab]

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