tendsto_toNNReal_atTop_iff — Mathlib

English

For any l, Tendsto (λ x, x.toNNReal) l atTop ⇔ Tendsto x l atTop.

Русский

Для любого l: Tendsto (λ x, x.toNNReal) l atTop ⇔ Tendsto x l atTop.

LaTeX

$$$\\text{Tendsto} (\\lambda x. x.toNNReal) l atTop \\iff \\text{Tendsto} x l atTop$$$

Lean4

@[simp]
theorem _root_.Real.tendsto_toNNReal_atTop_iff {l : Filter α} {f : α → ℝ} :
    Tendsto (fun x ↦ (f x).toNNReal) l atTop ↔ Tendsto f l atTop := by
  rw [← Real.comap_toNNReal_atTop, tendsto_comap_iff, Function.comp_def]

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