progMeasurable_of_tendsto — Mathlib

English

Specialization: if U: Nat → ι → Ω → β are ProgMeasurable and Tendsto U atTop to u, then u is ProgMeasurable.

Русский

Специализация: если U: Nat → ι → Ω → β прогрессивно измеримы и сходятся по atTop к u, тогда u прогрессивно измерим.

LaTeX

$$$(\\forall n,\\mathrm{ProgMeasurable}(f, U n)) \\Rightarrow \\mathrm{Tendsto}\\ U\\ atTop\\ (\\mathcal N\\ u) \\Rightarrow \\mathrm{ProgMeasurable}(f, u)$$$

Lean4

theorem progMeasurable_of_tendsto [MeasurableSpace ι] [PseudoMetrizableSpace β] {U : ℕ → ι → Ω → β}
    (h : ∀ l, ProgMeasurable f (U l)) (h_tendsto : Tendsto U atTop (𝓝 u)) : ProgMeasurable f u :=
  progMeasurable_of_tendsto' atTop h h_tendsto

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