tendsto_IicSnd_atTop — Mathlib

English

For measurable s, the function r ↦ ρ.IicSnd r s tends to ρ.fst s as r → ∞ (along rationals).

Русский

Для измеримого множества s функция r ↦ ρ.IicSnd r s стремится к ρ.fst s при r → ∞ (по рациональным).

LaTeX

$$$\mathrm{Tendsto}\left(\lambda r. ρ.IicSnd r s\right)\;\mathrm{atTop}\; (\mathcal{N}(ρ.fst s))$$$

Lean4

theorem tendsto_IicSnd_atTop {s : Set α} (hs : MeasurableSet s) :
    Tendsto (fun r : ℚ ↦ ρ.IicSnd r s) atTop (𝓝 (ρ.fst s)) :=
  by
  simp_rw [ρ.IicSnd_apply _ hs, fst_apply hs, ← prod_univ]
  rw [← Real.iUnion_Iic_rat, prod_iUnion]
  apply tendsto_measure_iUnion_atTop
  exact monotone_const.set_prod Rat.cast_mono.Iic

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