compl_bot

Mathlib.Order.Heyting.Basic

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

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem compl_bot : (⊥ : α)ᶜ = ⊤ := by rw [← himp_bot, himp_self]

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

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

Разделы

Аффилиация

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