disjoint_iff

Mathlib.Order.Disjoint

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

English

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

Русский

Если a и b несовместимы, тогда a ∧ b ≤ ⊥.

LaTeX

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

Lean4

theorem disjoint_iff : Disjoint a b ↔ a ⊓ b = ⊥ :=
  disjoint_iff_inf_le.trans le_bot_iff

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

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

Разделы

Аффилиация

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