congr — Mathlib

English

If X equals Y almost everywhere with respect to ℙ, then HasPDF X ℙ μ implies HasPDF Y ℙ μ.

Русский

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

LaTeX

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

Lean4

theorem congr (hXY : X =ᵐ[ℙ] Y) [hX : HasPDF X ℙ μ] : HasPDF Y ℙ μ :=
  ⟨(HasPDF.aemeasurable X ℙ μ).congr hXY, ℙ.map_congr hXY ▸ hX.haveLebesgueDecomposition,
    ℙ.map_congr hXY ▸ hX.absolutelyContinuous⟩

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