English
A limit (in a general filter) of measurable functions valued in a (pseudo) metrizable space is measurable.
Русский
Предел (для произвольного фильтра) последовательности измеримых функций, значение которой лежит в метрическом пространстве, в метрическом случае измерим.
LaTeX
$$$\\text{measurable\_of\_tendsto\_metrizable'}(u, f_i, g)$$$
Lean4
/-- A limit (over a general filter) of measurable functions valued in a (pseudo) metrizable space is
measurable. -/
theorem measurable_of_tendsto_metrizable' {ι} {f : ι → α → β} {g : α → β} (u : Filter ι) [NeBot u]
[IsCountablyGenerated u] (hf : ∀ i, Measurable (f i)) (lim : Tendsto f u (𝓝 g)) : Measurable g :=
by
letI : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
apply measurable_of_isClosed'
intro s h1s h2s h3s
have : Measurable fun x => infNndist (g x) s :=
by
suffices Tendsto (fun i x => infNndist (f i x) s) u (𝓝 fun x => infNndist (g x) s) from
NNReal.measurable_of_tendsto' u (fun i => (hf i).infNndist) this
rw [tendsto_pi_nhds] at lim ⊢
intro x
exact ((continuous_infNndist_pt s).tendsto (g x)).comp (lim x)
have h4s : g ⁻¹' s = (fun x => infNndist (g x) s) ⁻¹' {0} :=
by
ext x
simp [← h1s.mem_iff_infDist_zero h2s, ← NNReal.coe_eq_zero]
rw [h4s]
exact this (measurableSet_singleton 0)
