inf_bot_eq

Mathlib.Order.BoundedOrder.Lattice

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

English

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

Русский

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

LaTeX

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

Lean4

theorem inf_bot_eq (a : α) : a ⊓ ⊥ = ⊥ :=
  inf_of_le_right bot_le

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

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

Разделы

Аффилиация

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