English
The set of x for which a sequence of measurable functions tends to a limit is measurable.
Русский
Множество точек, где последовательность измеримых функций сходится, измеримо.
LaTeX
$$MeasurableSet {x | Tendsto (f_n x) l (nhds c)}$$
Lean4
/-- The set of points for which a sequence of measurable functions converges to a given function
is measurable. -/
@[measurability]
theorem measurableSet_tendsto_fun [MeasurableSpace γ] [Countable ι] {l : Filter ι} [l.IsCountablyGenerated]
[TopologicalSpace γ] [SecondCountableTopology γ] [PseudoMetrizableSpace γ] [OpensMeasurableSpace γ] {f : ι → β → γ}
(hf : ∀ i, Measurable (f i)) {g : β → γ} (hg : Measurable g) :
MeasurableSet {x | Tendsto (fun n ↦ f n x) l (𝓝 (g x))} :=
by
letI := TopologicalSpace.pseudoMetrizableSpacePseudoMetric γ
simp_rw [tendsto_iff_dist_tendsto_zero (f := fun n ↦ f n _)]
exact measurableSet_tendsto (𝓝 0) (fun n ↦ (hf n).dist hg)
