le_bot

Mathlib.Order.Disjoint

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

English

Disjoint a b implies a ∧ b = ⊥.

Русский

Несовместимость a и b влечет равенство их meet нулю: a ∧ b = ⊥.

LaTeX

$$$Disjoint\ a\ b \Rightarrow a \wedge b = \bot$$$

Lean4

theorem le_bot : Disjoint a b → a ⊓ b ≤ ⊥ :=
  disjoint_iff_inf_le.mp

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

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

Разделы

Аффилиация

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