bot_codisjoint

Mathlib.Order.Disjoint

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

English

In a bounded lattice, Codisjoint ⊥ a is equivalent to a = ⊤.

Русский

В ограниченной решётке Codisjoint ⊥ a эквивалентно a = ⊤.

LaTeX

$$$\operatorname{Codisjoint}(\bot,a) \iff a = \top$$$

Lean4

@[simp]
theorem bot_codisjoint : Codisjoint ⊥ a ↔ a = ⊤ :=
  ⟨fun h ↦ top_unique <| h bot_le le_rfl, fun h _ _ ha ↦ h.symm.trans_le ha⟩

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

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

Разделы

Аффилиация

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