tendsto_Iio_atTop — Mathlib

English

Dual statement for Iio: Tendsto from atTop is equivalent to Tendsto to the left neighborhood at a.

Русский

Двойственная формулировка Iio: пределы от atTop эквивалентны пределу слева в a.

LaTeX

$$$\\mathrm{Tendsto}(f)\\;\\mathrm{atTop} \\iff \\mathrm{Tendsto}(f)\\;\\mathcal{N}_{<}(a)$$$

Lean4

@[simp]
theorem tendsto_Iio_atTop {f : β → Iio a} : Tendsto f l atTop ↔ Tendsto (fun x => (f x : α)) l (𝓝[<] a) := by
  rw [← comap_coe_Iio_nhdsLT, tendsto_comap_iff]; rfl

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