map_inv_atBot — Mathlib

English

The inversion map induces equalities between maps on filters: map inv of atBot equals atTop, and map inv of atTop equals atBot, under an appropriate ordered group structure.

Русский

Отображение инверсии индуцирует равенства между отображениями на фильтрах: image(inv) от atBot равно atTop, и image(inv) от atTop равно atBot, при соответствующей структуре упорядоченной группы.

LaTeX

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

Lean4

@[to_additive]
theorem map_inv_atBot : map (Inv.inv : G → G) atBot = atTop :=
  (OrderIso.inv G).map_atBot

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