eq_bot

Mathlib.Order.Disjoint

URI: https://scilib.ai/kg/mathlib#Disjoint.eq_bot

English

If a and b are disjoint, then a ∧ b = ⊥.

Русский

Если a и b несовместимы, то их meet равен ⊥.

LaTeX

$$Disjoint a b → a ∧ b = ⊥$$

Lean4

theorem eq_bot : Disjoint a b → a ⊓ b = ⊥ :=
  bot_unique ∘ Disjoint.le_bot

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

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

Разделы

Аффилиация

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