comap_atTop — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem comap_atTop (e : α ≃o β) : comap e atTop = atTop := by simp [atTop, ← e.surjective.iInf_comp]

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