eq_bot_of_ge

Mathlib.Order.Disjoint

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

English

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

Русский

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

LaTeX

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

Lean4

theorem eq_bot_of_ge (hab : Disjoint a b) : b ≤ a → b = ⊥ :=
  hab.symm.eq_bot_of_le

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

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

Разделы

Аффилиация

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