map_sup

Mathlib.Order.Sublattice

URI: https://scilib.ai/kg/mathlib#Sublattice.map_sup

English

The image of the top Sublattice under a surjective homomorphism is the top Sublattice: map f ⊤ = ⊤.

Русский

Образ верхнего элемента под сюрьективным гомоморфизмом — это верхний элемент: map f ⊤ = ⊤.

LaTeX

$$Sublattice.map f ⊤ = ⊤$$

Lean4

theorem map_sup (f : LatticeHom α β) (L M : Sublattice α) : (L ⊔ M).map f = L.map f ⊔ M.map f :=
  (gc_map_comap f).l_sup

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru