tendsto_comp_coe_Iio_atTop — Mathlib

English

Dual to Iio atTop, Tendsto from atTop corresponds to Tendsto to the left neighborhood of a.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem tendsto_comp_coe_Iio_atTop : Tendsto (fun x : Iio a => f x) atTop l ↔ Tendsto f (𝓝[<] a) l := by
  rw [← map_coe_Iio_atTop, tendsto_map'_iff]; rfl

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