top_sup_eq

Mathlib.Order.BoundedOrder.Lattice

URI: https://scilib.ai/kg/mathlib#top_sup_eq

English

In a lattice with a top element, the join of the top with any element is the top: ⊤ ⊔ a = ⊤.

Русский

В решётке с верхней границей объединение верхней границы с любым элементом даёт верхнюю границу: ⊤ ⊔ a = ⊤.

LaTeX

$$$\\top_{\\alpha} \\;\\; ⊔ \\;\\; a = \\top_{\\alpha}$$$

Lean4

theorem top_sup_eq (a : α) : ⊤ ⊔ a = ⊤ :=
  sup_of_le_left le_top

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

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

Разделы

Аффилиация

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