hnot_boundary

Mathlib.Order.Heyting.Boundary

URI: https://scilib.ai/kg/mathlib#Coheyting.hnot_boundary

English

In a co-Heyting algebra, for every element a, the negation of the boundary of a is the top element.

Русский

В ко-Хейтинговой алгебре для любого элемента a отрицание границы a равно верхнему элементу.

LaTeX

$$$ \forall a:\alpha, \neg \partial a = \top $$$

Lean4

@[simp]
theorem hnot_boundary (a : α) : ￢∂ a = ⊤ := by rw [boundary, hnot_inf_distrib, sup_hnot_self]

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

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

Разделы

Аффилиация

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