English
Let G be a commutative group with a compatible order. For any index set α, any filter l on α, and any function f: α → G, the tendence of the inverse of f along l to the bottom of the order is equivalent to the tendence of f along l to the top: (f x)^{-1} → atBot iff f x → atTop.
Русский
Пусть G — коммутативная группа с совместимой с порядком структурой. Пусть α — множество индексов, l — фильтр на α, f: α → G. Тогда предел во времени стремления последовательности f(x) к верхней границе эквивалентен пределу ее обратного элемента к нижней границе: f(x)^{-1} → atBot эквивалентно f(x) → atTop.
LaTeX
$$$\\forall {\\alpha} {G} [\\text{CommGroup } G] [\\text{PartialOrder } G] [\\text{IsOrderedMonoid } G] \\forall l : \\text{Filter } \\alpha \\; \\forall f : \\alpha \\to G,\\; \\operatorname{Tendsto}(\\lambda x. f(x)^{-1})\,l\\,\\operatorname{atBot} \\;\\iff\\; \\operatorname{Tendsto} f\,l\\,\\operatorname{atTop}$$$
Lean4
@[to_additive (attr := simp)]
theorem tendsto_inv_atBot_iff : Tendsto (fun x => (f x)⁻¹) l atBot ↔ Tendsto f l atTop :=
(OrderIso.inv G).tendsto_atTop_iff
