measureReal_congr — Mathlib

English

If two sets are almost everywhere equal with respect to μ, then their real measures coincide: μ.real s = μ.real t.

Русский

Если два множества равны почти повсюду относительно μ, то их вещественные меры равны: μ.real s = μ.real t.

LaTeX

$$$ s =_{\\text{ae}}^{\\mu} t \\quad \\Rightarrow \\quad \\mu.real s = \\mu.real t $$$

Lean4

/-- If two sets are equal modulo a set of measure zero, then `μ.real s = μ.real t`. -/
theorem measureReal_congr (H : s =ᵐ[μ] t) : μ.real s = μ.real t := by simp [Measure.real, measure_congr H]

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