hnot_eq_sInf_codisjoint

Mathlib.Order.CompleteBooleanAlgebra

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

English

The Heyting negation of a equals the infimum of those w that are codisjoint with a.

Русский

Отрицание Хейтинга a равно инфимума тех w, которые кодисjoint с a.

LaTeX

$$$\neg a = \operatorname{sInf} \{ w \mid \operatorname{Codisjoint}(a,w) \}$$$

Lean4

theorem hnot_eq_sInf_codisjoint : ￢a = sInf {w | Codisjoint a w} :=
  (isLeast_hnot a).isGLB.sInf_eq.symm

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

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

Разделы

Аффилиация

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