tendsto_atTop_iff — Mathlib

English

Under an order topology, for u ~_l v, tendsto atTop holds for u if and only if it holds for v.

Русский

При топологии порядка для u ~_l v, сходится к бесконечности для u тогда и только тогда, когда сходится для v.

LaTeX

$$$ \\forall u, v: (u \\sim_{l} v) \\Rightarrow (\\mathrm{Tendsto}\\ u\\ l\\ \\mathrm{atTop}) \\iff (\\mathrm{Tendsto}\\ v\\ l\\ \\mathrm{atTop}) $$$

Lean4

theorem tendsto_atTop_iff [OrderTopology β] (huv : u ~[l] v) : Tendsto u l atTop ↔ Tendsto v l atTop :=
  ⟨huv.tendsto_atTop, huv.symm.tendsto_atTop⟩

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