sup_bot_eq

Mathlib.Order.BoundedOrder.Lattice

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

English

In a semilattice with bottom, the meet with bottom yields bottom: a ⊓ ⊥ = ⊥.

Русский

В полурешётке с нулём пересечение с нижней границей даёт нижнюю границу: a ⊓ ⊥ = ⊥.

LaTeX

$$$a \\;⊓\\; \\bot = \\bot$$$

Lean4

theorem sup_bot_eq (a : α) : a ⊔ ⊥ = a :=
  sup_of_le_left bot_le

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

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

Разделы

Аффилиация

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