map_atTop — Mathlib

English

If e is an order isomorphism, then pushing forward the filter atTop along e yields atTop: map (e) atTop = atTop.

Русский

Если e — порядок-изоморфизм, то отображение фильтра на вершину сохраняется: map(e) atTop = atTop.

LaTeX

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

Lean4

@[simp]
theorem map_atTop (e : α ≃o β) : map (e : α → β) atTop = atTop := by
  rw [← e.comap_atTop, map_comap_of_surjective e.surjective]

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