compl_eq_sSup_disjoint

Mathlib.Order.CompleteBooleanAlgebra

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

English

In a frame, the complement a^c equals the supremum of all w disjoint from a.

Русский

В рамке комплемент a^c равен верхнему пределу всех w, несовместимых с a.

LaTeX

$$$a^{\complement} = \operatorname{sSup} \{ w \mid \operatorname{Disjoint}(w,a)\}$$$

Lean4

theorem compl_eq_sSup_disjoint : aᶜ = sSup {w | Disjoint w a} :=
  (isGreatest_compl a).isLUB.sSup_eq.symm

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

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

Разделы

Аффилиация

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