intervalIntegrable_congr_ae — Mathlib

English

If two functions are codiscretely almost-everywhere equal on Ι(a,b), then they have the same interval integrability property.

Русский

Если две функции совпадают почти всегда в кодискретном смысле на Ι(a,b), то их интервальная интегрируемость совпадает.

LaTeX

$$$$\text{IntervalIntegrable}(f,μ,a,b) \iff \text{IntervalIntegrable}(g,μ,a,b)$$ under codiscreteWithin equality.$$

Lean4

theorem intervalIntegrable_congr_ae {g : ℝ → ε} (h : f =ᵐ[μ.restrict (Ι a b)] g) :
    IntervalIntegrable f μ a b ↔ IntervalIntegrable g μ a b := by
  rw [intervalIntegrable_iff, integrableOn_congr_fun_ae h, intervalIntegrable_iff]

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