comap — Mathlib

English

Pullback of an outer measure along f: comap f μ is the outer measure on α defined by comap f μ (s) = μ(f'' s).

Русский

Обратное по отображению внешней меры вдоль f: comap f μ — внешняя мера на α, заданная как comap f μ (s) = μ(f'' s).

LaTeX

$$$ (comap\ f\ \mu)(S) = \mu(f''\!S) $$$

Lean4

/-- Pullback of an `OuterMeasure`: `comap f μ s = μ (f '' s)`. -/
def comap {β} (f : α → β) : OuterMeasure β →ₗ[ℝ≥0∞] OuterMeasure α
    where
  toFun
    m :=
    { measureOf := fun s => m (f '' s)
      empty := by simp
      mono := fun {_ _} h => by gcongr
      iUnion_nat := fun s _ => by simpa only [image_iUnion] using measure_iUnion_le _ }
  map_add' _ _ := rfl
  map_smul' _ _ := rfl

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