tendsto_inv_atTop_atBot — Mathlib

English

The inversion map sends Tendsto toTop to Tendsto toBot and vice versa in a filtered setting of a group with order.

Русский

Инверсия переводит предел к верху в предел к низу и наоборот в фильтрованной группе с порядком.

LaTeX

$$$\\mathrm{Tendsto}(\\mathrm{Inv.inv})\\mathrm{atTop}\\;\\mathrm{atBot}$$$

Lean4

@[to_additive]
theorem tendsto_inv_atTop_atBot : Tendsto (Inv.inv : G → G) atTop atBot :=
  (OrderIso.inv G).tendsto_atTop

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