compl_inf

Mathlib.Order.UpperLower.CompleteLattice

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

English

Complement distributes over inf for lower sets: (s ⊓ t).compl = s.compl ⊓ t.compl.

Русский

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

LaTeX

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

Lean4

protected theorem compl_inf (s t : LowerSet α) : (s ⊓ t).compl = s.compl ⊓ t.compl :=
  UpperSet.ext compl_inf

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

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

Разделы

Аффилиация

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