eq_top

Mathlib.Order.Disjoint

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

English

In a semilattice with top, Codisjoint a b implies a ⊔ b = ⊤.

Русский

В полусоединённой решётке Codisjoint a b влечёт a ⊔ b = ⊤.

LaTeX

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

Lean4

theorem eq_top : Codisjoint a b → a ⊔ b = ⊤ :=
  @Disjoint.eq_bot αᵒᵈ _ _ _ _

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

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

Разделы

Аффилиация

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