tendsto_atBot_iff — Mathlib

English

For equivalent functions, tendsto to atBot holds for one if and only if it holds for the other.

Русский

Для эквивалентных функций сходится к atBot тогда и только тогда, когда сходится другая функция.

LaTeX

$$$ (u \\sim_{l} v) \\Rightarrow (Tendsto u l atBot) \\Leftrightarrow (Tendsto v l atBot) $$$

Lean4

theorem tendsto_atBot_iff [OrderTopology β] (huv : u ~[l] v) : Tendsto u l atBot ↔ Tendsto v l atBot :=
  ⟨huv.tendsto_atBot, huv.symm.tendsto_atBot⟩

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