dual_le_dual

Mathlib.Analysis.Convex.Cone.Dual

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

English

The dual of a union over an index is the infimum of the duals: dual(p, ⋃ i f(i)) = inf_i dual(p, f(i)).

Русский

Дуал объединения по индексу равен наименьшему (пересечению) дуалам: dual(p, ⋃ i f(i)) = ⨅ i dual(p, f(i)).

LaTeX

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

Lean4

@[gcongr]
theorem dual_le_dual (h : t ⊆ s) : dual p s ≤ dual p t := fun _y hy _x hx ↦ hy (h hx)

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

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

Разделы

Аффилиация

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