tendsto_pre_nat — Mathlib

English

The tendsto of pre m with respect to n⁻¹ converges to mkMetric' m as n → ∞.

Русский

Пределы предела pre m при n⁻¹ сходятся к mkMetric' m при n → ∞.

LaTeX

$$$\\mathrm{tendsto}\\, (\\lambda n: \\mathrm{pre}\\, m\\, n^{-1})\\, \\text{atTop} \\; (\\mathfrak{n} ) = mkMetric' m$$

Lean4

theorem tendsto_pre_nat (m : Set X → ℝ≥0∞) (s : Set X) :
    Tendsto (fun n : ℕ => pre m n⁻¹ s) atTop (𝓝 <| mkMetric' m s) :=
  by
  refine (tendsto_pre m s).comp (tendsto_inf.2 ⟨ENNReal.tendsto_inv_nat_nhds_zero, ?_⟩)
  refine tendsto_principal.2 (Eventually.of_forall fun n => ?_)
  simp

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