comap_map — Mathlib

English

For a measurable embedding f, almost everywhere behavior of p under μ.map f is equivalent to the a.e. behavior of p ∘ f under μ.

Русский

Для измеримого вложения f, поведение почти всюду для p после отображения μ.map f эквивалентно поведеню p ∘ f почти всюду по μ.

LaTeX

$$$\forall p,\; (\forall^{\mathrm{ae}} x \partial μ.map f, p x) \iff (\forall^{\mathrm{ae}} x \partial μ, p(f x)).$$$

Lean4

theorem comap_map (μ : Measure α) : (map f μ).comap f = μ :=
  by
  ext t _
  rw [hf.comap_apply, hf.map_apply, preimage_image_eq _ hf.injective]

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