eq_bot_of_le

Mathlib.Order.Disjoint

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

English

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

Русский

Если a и b несовместны и a ≤ b, то a = ⊥.

LaTeX

$$$(a \wedge b = \bot) \land (a \le b) \Rightarrow a = \bot$$$

Lean4

theorem eq_bot_of_le (hab : Disjoint a b) (h : a ≤ b) : a = ⊥ :=
  eq_bot_iff.2 <| hab le_rfl h

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

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

Разделы

Аффилиация

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