compl_sup

Mathlib.Order.UpperLower.CompleteLattice

URI: https://scilib.ai/kg/mathlib#LowerSet.compl_sup

English

Complement distributes over sup for lower sets: (s ⊔ t).compl = s.compl ⊔ t.compl.

Русский

Комплемент распределяется через объединение нижних множеств: (s ⊔ t).compl = s.compl ⊔ t.compl.

LaTeX

$$$(s \sqcup t).\mathrm{compl} = s.\mathrm{compl} \sqcup t.\mathrm{compl}$$$

Lean4

protected theorem compl_sup (s t : LowerSet α) : (s ⊔ t).compl = s.compl ⊔ t.compl :=
  UpperSet.ext compl_sup

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

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

Разделы

Аффилиация

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