tendsto_atBot — Mathlib

English

If u ~_l v, then the negative of u tends to atTop if the negative of v tends to atTop, and vice versa.

Русский

Если u эквивалентно v по l, тогда -u имеет тенденцию к atTop, если -v имеет тенденцию к atTop, и наоборот.

LaTeX

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

Lean4

theorem tendsto_atBot [OrderTopology β] (huv : u ~[l] v) (hu : Tendsto u l atBot) : Tendsto v l atBot :=
  by
  convert tendsto_neg_atTop_atBot.comp (huv.neg.tendsto_atTop <| tendsto_neg_atBot_atTop.comp hu)
  ext
  simp

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