comap_inv_atTop — Mathlib

English

In an ordered group, comap of inversion maps atTop to atBot and vice versa; the comap respects the order-reversing nature of inversion.

Русский

В упорядоченной группе comap инверсии отображает atTop в atBot и обратно; comap сохраняет противоположную по порядку природу инверсии.

LaTeX

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

Lean4

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

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