congr_iff — Mathlib

English

X ≈ Y almost everywhere (with respect to ℙ) if and only if HasPDF X ℙ μ is equivalent to HasPDF Y ℙ μ.

Русский

X эквивалентны почти всюду Y по отношению к ℙ тогда и только тогда, когда HasPDF X ℙ μ эквивалентно HasPDF Y ℙ μ.

LaTeX

$$$(X =^{\\mathrm{a.e.}}_{\\ℙ} Y) \\iff (HasPDF X \\ℙ μ \\iff HasPDF Y \\ℙ μ)$$$

Lean4

theorem congr_iff (hXY : X =ᵐ[ℙ] Y) : HasPDF X ℙ μ ↔ HasPDF Y ℙ μ :=
  ⟨fun _ ↦ HasPDF.congr hXY, fun _ ↦ HasPDF.congr hXY.symm⟩

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