English
A limit (over a general filter) of measurable ℝ≥0-valued functions is measurable.
Русский
Предел функции, принимающей значения ℝ≥0 и являющейся пределом последовательности измеримых функций (по произвольному фильтру), измерим.
LaTeX
$$$\\text{Theorem: }\\ \\text{measurable_of_tendsto'}\n \\text{for } f: \\iota \\to X \\to \\mathbb{R}_{\\ge 0}$$$
Lean4
/-- A limit (over a general filter) of measurable `ℝ≥0`-valued functions is measurable. -/
theorem measurable_of_tendsto' {ι} {f : ι → α → ℝ≥0} {g : α → ℝ≥0} (u : Filter ι) [NeBot u] [IsCountablyGenerated u]
(hf : ∀ i, Measurable (f i)) (lim : Tendsto f u (𝓝 g)) : Measurable g :=
by
simp_rw [← measurable_coe_nnreal_ennreal_iff] at hf ⊢
refine ENNReal.measurable_of_tendsto' u hf ?_
rw [tendsto_pi_nhds] at lim ⊢
exact fun x => (ENNReal.continuous_coe.tendsto (g x)).comp (lim x)
