comap' — Mathlib

English

Comap of μ along a continuous embedding preserves finiteness-on-compacts.

Русский

Комап меры по непрерывному вложению сохраняет конечность на компактных.

LaTeX

$$$IsFiniteMeasureOnCompacts (\mu \circ f)$$$

Lean4

protected theorem comap' [TopologicalSpace α] [TopologicalSpace β] (μ : Measure β) [IsFiniteMeasureOnCompacts μ]
    {f : α → β} (f_cont : Continuous f) (f_me : MeasurableEmbedding f) : IsFiniteMeasureOnCompacts (μ.comap f) where
  lt_top_of_isCompact K
    hK := by
    rw [f_me.comap_apply]
    exact IsFiniteMeasureOnCompacts.lt_top_of_isCompact (hK.image f_cont)

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