compl_top

Mathlib.Order.Heyting.Basic

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

English

In a Heyting algebra, the complement of the top element is the bottom: ⊤ᶜ = ⊥.

Русский

В Хейтинговой алгебре комплемент верхнего элемента равен нижнему: ⊤ᶜ = ⊥.

LaTeX

$$$\top^{\complement} = \bot$$$

Lean4

@[simp]
theorem compl_top : (⊤ : α)ᶜ = ⊥ :=
  eq_of_forall_le_iff fun a => by rw [le_compl_iff_disjoint_right, disjoint_top, le_bot_iff]

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

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

Разделы

Аффилиация

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