English
If U l are ProgMeasurable and U converges to u along a filter, then u is ProgMeasurable.
Русский
Если U литеры прогрессивно измеримы и сходятся к u по фильтру, то u прогрессивно измерим.
LaTeX
$$$(\\forall l,\\mathrm{ProgMeasurable}(f, U l)) \\Rightarrow \\mathrm{Tendsto}\\ U\\ fltr\\ (\\mathcal N\\ u) \\Rightarrow \\mathrm{ProgMeasurable}(f, u)$$$
Lean4
theorem progMeasurable_of_tendsto' {γ} [MeasurableSpace ι] [PseudoMetrizableSpace β] (fltr : Filter γ) [fltr.NeBot]
[fltr.IsCountablyGenerated] {U : γ → ι → Ω → β} (h : ∀ l, ProgMeasurable f (U l))
(h_tendsto : Tendsto U fltr (𝓝 u)) : ProgMeasurable f u :=
by
intro i
apply
@stronglyMeasurable_of_tendsto (Set.Iic i × Ω) β γ (MeasurableSpace.prod _ (f i)) _ _ fltr _ _ _ _ fun l => h l i
rw [tendsto_pi_nhds] at h_tendsto ⊢
intro x
specialize h_tendsto x.fst
rw [tendsto_nhds] at h_tendsto ⊢
exact fun s hs h_mem => h_tendsto {g | g x.snd ∈ s} (hs.preimage (continuous_apply x.snd)) h_mem
