disjoint_of_le_iff_left_eq_bot

Mathlib.Order.Disjoint

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

English

If a ≤ b, then a and b are disjoint if and only if a = ⊥.

Русский

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

LaTeX

$$$a \le b \Rightarrow (Disjoint\ a\ b \iff a = \bot)$$$

Lean4

theorem disjoint_of_le_iff_left_eq_bot (h : a ≤ b) : Disjoint a b ↔ a = ⊥ :=
  ⟨fun hd ↦ hd.eq_bot_of_le h, fun h ↦ h ▸ disjoint_bot_left⟩

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

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

Разделы

Аффилиация

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