tendsto_inv_atTop_iff — Mathlib

English

Let l be a filter on α and G a commutative group with order. The tendsto of the inverse of f is equivalent to tendsto f to the bottom: Tendsto inv f l atTop iff Tendsto f l atBot.

Русский

Пусть l — фильтр на α и G — коммутативная группа с порядком. Стремление обратного элемента эквивалентно стремлению функции к дну: Tendsto inv f l atTop ⇔ Tendsto f l atBot.

LaTeX

$$$\\text{Tendsto}(\\lambda x, f(x)^{-1})\\ l\\ \\mathrm{atTop} \\iff \\text{Tendsto}(f)\\ l\\ \\mathrm{atBot}$$$

Lean4

@[to_additive (attr := simp)]
theorem tendsto_inv_atTop_iff : Tendsto (fun x => (f x)⁻¹) l atTop ↔ Tendsto f l atBot :=
  (OrderIso.inv G).tendsto_atBot_iff

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