map_of_continuous — Mathlib

English

Continuous pushforward preserves inner regularity for compact LTTop measures.

Русский

Плотно непрерывное отображение сохраняет внутреннюю регулярность для мер с компактной LTTop.

LaTeX

$$$f:\alpha\to\beta\;\text{ continuous} \Rightarrow μ\mapsto f_*μ \text{ preserves InnerRegularCompactLTTop}$$$

Lean4

protected theorem map_of_continuous [BorelSpace α] [MeasurableSpace β] [TopologicalSpace β] [BorelSpace β]
    [h : InnerRegularCompactLTTop μ] {f : α → β} (hf : Continuous f) : InnerRegularCompactLTTop (Measure.map f μ) :=
  by
  constructor
  refine InnerRegularWRT.map h.innerRegular hf.aemeasurable ?_ (fun K hK ↦ hK.image hf) ?_
  · rintro s ⟨hs, h's⟩
    exact ⟨hf.measurable hs, by rwa [map_apply hf.measurable hs] at h's⟩
  · rintro s ⟨hs, -⟩
    exact hs

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