boundary_hnot_hnot

Mathlib.Order.Heyting.Boundary

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

English

Double negation boundary invariance: ∂(¬¬a) = ∂(¬a).

Русский

Инвариантность границы двойного отрицания: ∂(¬¬a) = ∂(¬a).

LaTeX

$$$\partial(\\neg\\neg a) = \partial(\\neg a)$$$

Lean4

@[simp]
theorem boundary_hnot_hnot (a : α) : ∂ (￢￢a) = ∂ (￢a) := by simp_rw [boundary, hnot_hnot_hnot, inf_comm]

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

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

Разделы

Аффилиация

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