map_top — Mathlib

English

The comap of the top under an isomorphism equals the top under the corresponding map.

Русский

Обратный образ верхнего элемента под изоморфизмом равен верхнему элементу под соответствующим отображением.

LaTeX

$$Sublattice.comap f ⊤ = ⊤$$

Lean4

theorem map_top (f : LatticeHom α β) (h : Surjective f) : Sublattice.map f ⊤ = ⊤ :=
  SetLike.coe_injective <| by simp [h.range_eq]

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