continuous_map — Mathlib

English

If ν_s → ν in FiniteMeasure and f is continuous, then the push-forward ν_s.map f → ν.map f.

Русский

Если ν_s сходится к ν, а f непрерывна, то ν_s.map f сходится к ν.map f.

LaTeX

$$$Tendsto ν_s L (nhds ν) \\Rightarrow Tendsto (fun i => ν_s i.map f) L (nhds (ν.map f))$ for continuous f$$

Lean4

/-- If `f : X → Y` is continuous and `Y` is equipped with the Borel sigma algebra, then
the push-forward of finite measures `f* : FiniteMeasure X → FiniteMeasure Y` is continuous
(in the topologies of weak convergence of measures). -/
theorem continuous_map {f : Ω → Ω'} (f_cont : Continuous f) : Continuous (fun ν ↦ FiniteMeasure.map ν f) :=
  by
  rw [continuous_iff_continuousAt]
  exact fun _ ↦ tendsto_map_of_tendsto_of_continuous _ _ continuous_id.continuousAt f_cont

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