comap — Mathlib

English

Pushforward of a finite-on-compacts measure by a homeomorphism preserves the finite-on-compacts property.

Русский

Объединение меры, конечной на компактах, через гомеморфизм сохраняет свойство конечности на компактах.

LaTeX

$$$\\\\operatorname{IsFiniteMeasureOnCompacts}(\\\\mu.map f)$$$

Lean4

protected theorem comap (μ : Measure β) [IsFiniteMeasureOnCompacts μ] (f : α ≃ₜ β) :
    IsFiniteMeasureOnCompacts (μ.comap f) :=
  IsFiniteMeasureOnCompacts.comap' μ f.continuous f.measurableEmbedding

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