map_top — Mathlib

English

Let f be a surjective bounded lattice homomorphism between α and β. Then the image of the top element is the top element: map f ⊤ = ⊤.

Русский

Пусть f — сюръективный гомоморфизм ограниченной решётки между α и β. Тогда образ вершины равен вершине: map f ⊤ = ⊤.

LaTeX

$$$\\operatorname{map} f \\top = \\top$$$

Lean4

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

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