congr — Mathlib

English

If f and g are equal almost everywhere, AEStronglyMeasurable f μ implies AEStronglyMeasurable g μ and vice versa.

Русский

Если f и g равны почти повсюду, то AEStronglyMeasurable f μ и AEStronglyMeasurable g μ взаимно переходят друг от друга.

LaTeX

$$$(f =^\\mu g) \\Rightarrow (AEStronglyMeasurable f \\mu \\Rightarrow AEStronglyMeasurable g \\mu)$$$

Lean4

theorem congr (hf : AEStronglyMeasurable[m] f μ) (h : f =ᵐ[μ] g) : AEStronglyMeasurable[m] g μ :=
  ⟨hf.mk f, hf.stronglyMeasurable_mk, h.symm.trans hf.ae_eq_mk⟩

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