boundary_eq_bot

Mathlib.Order.Heyting.Boundary

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

English

In a Boolean algebra, the boundary of any element is the bottom element: ∂ a = ⊥.

Русский

В булевой алгебре граница любого элемента равна нижнему элементу: ∂a = ⊥.

LaTeX

$$$ \partial a = \bot $$$

Lean4

@[simp]
theorem boundary_eq_bot (a : α) : ∂ a = ⊥ :=
  inf_compl_eq_bot

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

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

Разделы

Аффилиация

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