congr_ae — Mathlib

English

If two functions are almost everywhere equal on Ι(a,b), then they are interchangeable with respect to interval integrability.

Русский

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

LaTeX

$$$$\text{(f =ᵃᵉ μ|_{Ι(a,b)} g)} \Rightarrow \text{IntervalIntegrable}(f,μ,a,b) \iff \text{IntervalIntegrable}(g,μ,a,b).$$$$

Lean4

theorem congr_ae {g : ℝ → ε} (hf : IntervalIntegrable f μ a b) (h : f =ᵐ[μ.restrict (Ι a b)] g) :
    IntervalIntegrable g μ a b := by rwa [← intervalIntegrable_congr_ae h]

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