comap_atBot — Mathlib

English

If e is an order isomorphism, then pulling back the bottom filter along e yields the bottom filter: comap e atBot = atBot.

Русский

Если e — порядок-изоморфизм, то прообраз нижнего фильтра по e даёт нижний фильтр: comap e atBot = atBot.

LaTeX

$$$\\operatorname{comap}(e)\\operatorname{atBot} = \\operatorname{atBot}$$$

Lean4

@[simp]
theorem comap_atBot (e : α ≃o β) : comap e atBot = atBot :=
  e.dual.comap_atTop

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