dual_sUnion

Mathlib.Analysis.Convex.Cone.Dual

URI: https://scilib.ai/kg/mathlib#ProperCone.dual_sUnion

English

The dual of a family’s sUnion equals the infimum over the duals of the family.

Русский

Дуал семейства по отношению к сUnion равен наименьшему дуалу членов семейства.

LaTeX

$$dual p (⋃₀ S) = sInf (dual p '' S)$$

Lean4

theorem dual_sUnion (S : Set (Set M)) : dual p (⋃₀ S) = sInf (dual p '' S) := by ext; simp [forall_swap (α := M)]

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

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

Разделы

Аффилиация

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