comap_inv_atBot — Mathlib

English

In a ordered commutative group, the comap of the inversion map exchanges atBot and atTop: comap inv atBot = atTop.

Русский

В упорядоченной коммутативной группе отображение comap инверсии меняет нижний и верхний фильтр местами: comap inv atBot = atTop.

LaTeX

$$$\\mathrm{comap}(\\mathrm{Inv.inv})\\mathrm{atBot} = \\mathrm{atTop}$$$

Lean4

@[to_additive]
theorem comap_inv_atBot : comap (Inv.inv : G → G) atBot = atTop :=
  (OrderIso.inv G).comap_atTop

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