coe_toNNReal_ae_eq — Mathlib

English

If f is finite almost everywhere, then (f(x).toNNReal) considered in ENNReal equals f a.e.

Русский

Если f конечна почти всюду, то (f(x).toNNReal) как ENNReal совпадает с f по почти всей мере.

LaTeX

$$$(f:α→ENNReal)$ a.e. finite ⇒ (f(x).toNNReal:ENNReal) =_{ae} f(x)$$$

Lean4

theorem coe_toNNReal_ae_eq {f : α → ℝ≥0∞} (hf : ∀ᵐ x ∂μ, f x < ∞) : (fun x => ((f x).toNNReal : ℝ≥0∞)) =ᵐ[μ] f :=
  by
  filter_upwards [hf]
  intro x hx
  simp only [hx.ne, Ne, not_false_iff, coe_toNNReal]

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