map_inv_atTop — Mathlib

English

The inverse map on filters interchanges the top and bottom filters: map inv sends atTop to atBot and vice versa.

Русский

Инверсия отображения на фильтрах меняет верхний и нижний фильтры местами: image(inv) отправляет atTop в atBot и обратно.

LaTeX

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

Lean4

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

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