disjoint_top

Mathlib.Order.Disjoint

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

English

For α with a bounded order, Disjoint a with top equals bottom, i.e., a = ⊥.

Русский

Для множества с ограниченным порядком, несовместность a с верхушкой равна нижнему элементу: a = ⊥.

LaTeX

$$$Disjoint\ a\ top \iff a = \bot$$$

Lean4

@[simp]
theorem disjoint_top : Disjoint a ⊤ ↔ a = ⊥ :=
  ⟨fun h ↦ bot_unique <| h le_rfl le_top, fun h _ ha _ ↦ ha.trans_eq h⟩

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

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

Разделы

Аффилиация

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