lintegral_congr_ae — Mathlib

English

If f and g are equal almost everywhere with respect to μ, then their Lebesgue integrals are equal: ∫ f dμ = ∫ g dμ.

Русский

Если f и g равны почти всюду по отношению к μ, то их линегральные интегралы равны: ∫ f dμ = ∫ g dμ.

LaTeX

$$$\\int f \\, d\\mu = \\int g \\, d\\mu$$$

Lean4

theorem lintegral_congr_ae {f g : α → ℝ≥0∞} (h : f =ᵐ[μ] g) : ∫⁻ a, f a ∂μ = ∫⁻ a, g a ∂μ :=
  le_antisymm (lintegral_mono_ae <| h.le) (lintegral_mono_ae <| h.symm.le)

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