eq_top_of_le

Mathlib.Order.Disjoint

URI: https://scilib.ai/kg/mathlib#Codisjoint.eq_top_of_le

English

If Codisjoint a b and b ≤ a, then a = ⊤.

Русский

Если Codisjoint a b и b ≤ a, то a = ⊤.

LaTeX

$$$\operatorname{Codisjoint}(a,b) \to b \le a \to a = \top$$$

Lean4

theorem eq_top_of_le (hab : Codisjoint a b) (h : b ≤ a) : a = ⊤ :=
  eq_top_iff.2 <| hab le_rfl h

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

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

Разделы

Аффилиация

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