map_ofFunction_le — Mathlib

English

If f is injective, then map_ofFunction equality holds as an exact equality between pushforward of the ofFunction measure and ofFunction with preimage.

Русский

Если f инъективна, то равенство map_ofFunction выполняется как точное равенство образующей меры через pushforward и ofFunction с предобразами.

LaTeX

$$$\\text{map } f (\\text{OuterMeasure.ofFunction } m m\\_empty) = \\text{OuterMeasure.ofFunction } (\\lambda s. m (f^{-1}[s])) m\\_empty.$$$

Lean4

theorem map_ofFunction_le {β} (f : α → β) :
    map f (OuterMeasure.ofFunction m m_empty) ≤ OuterMeasure.ofFunction (fun s => m (f ⁻¹' s)) m_empty :=
  le_ofFunction.2 fun s => by
    rw [map_apply]
    apply ofFunction_le

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