compl_iSup

Mathlib.Order.CompleteBooleanAlgebra

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

English

Complement distributes over sup: (iSup f)ᶜ = iInf (f i)ᶜ.

Русский

Дополнение распределяется над объединением: (iSup f)ᶜ = ⨅ i (f i)ᶜ.

LaTeX

$$$\forall f,\; (\sup_i f(i))^{\complement} = \inf_i f(i)^{\complement}.$$$

Lean4

theorem compl_iSup : (iSup f)ᶜ = ⨅ i, (f i)ᶜ :=
  compl_injective (by simp [compl_iInf])

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

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

Разделы

Аффилиация

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