lintegral_eq_const — Mathlib

English

If μ is a probability measure and f is almost everywhere equal to a constant c, then the lintegral of f equals c.

Русский

Если μ является вероятностной мерой и f почти всюду равна константе c, тогда линегральный интеграл по f равен c.

LaTeX

$$$$\\int f \\, d\\mu = c \\quad\\text{если } f = c \\text{ почти всюду}.$$$$

Lean4

theorem lintegral_eq_const [IsProbabilityMeasure μ] {f : α → ℝ≥0∞} {c : ℝ≥0∞} (hf : ∀ᵐ x ∂μ, f x = c) :
    ∫⁻ x, f x ∂μ = c := by simp [lintegral_congr_ae hf]

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