map — Mathlib

English

The pushforward of an outer measure m along a function f : α → β is the outer measure on β defined by (map f m)(S) = m(f^{-1}(S)).

Русский

Пушфордовая внешняя мера по отображению f : α → β задаётся как (map f m)(S) = m(f^{-1}(S)).

LaTeX

$$$ (map\ f\ m)(S) = m(f^{-1}(S)) $$$

Lean4

/-- The pushforward of `m` along `f`. The outer measure on `s` is defined to be `m (f ⁻¹' s)`. -/
def map {β} (f : α → β) : OuterMeasure α →ₗ[ℝ≥0∞] OuterMeasure β
    where
  toFun
    m :=
    { measureOf := fun s => m (f ⁻¹' s)
      empty := m.empty
      mono := fun {_ _} h => m.mono (preimage_mono h)
      iUnion_nat := fun s _ => by simpa using measure_iUnion_le fun i => f ⁻¹' s i }
  map_add' _ _ := coe_fn_injective rfl
  map_smul' _ _ := coe_fn_injective rfl

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