dual_iUnion

Mathlib.Analysis.Convex.Cone.Dual

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

English

The dual of a union over an index is the infimum of duals of the sets (repeat).

Русский

Дуал объединения по индексу равен инфимину дуалов подмножеств (повторение).

LaTeX

$$dual p (⋃ i, f i) = ⨅ i, dual p (f i)$$

Lean4

theorem dual_iUnion {ι : Sort*} (f : ι → Set M) : dual p (⋃ i, f i) = ⨅ i, dual p (f i) := by ext;
  simp [forall_swap (α := M)]

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

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

Разделы

Аффилиация

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