le_sup_left

Mathlib.Order.Lattice

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

English

In any lattice with join, an element is always less than or equal to the join with another element: a ≤ a ∨ b.

Русский

В любой решётке с операцией объединения элемент всегда меньше или равен объединению с другим элементом: a ≤ a ∨ b.

LaTeX

$$$a \\le a \\lor b$$$

Lean4

@[simp]
theorem le_sup_left : a ≤ a ⊔ b :=
  SemilatticeSup.le_sup_left a b

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

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

Разделы

Аффилиация

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