English
Let f be a family of subsets f: ι → Set H. The dual cone of the union over i equals the intersection (infimum) of the dual cones: (⋃ i, f i).innerDualCone = ⨅ i, (f i).innerDualCone.
Русский
Пусть f: ι → Set H — семейство подмножеств. Дуальный конус объединения по индексу i равен пересечению (наименьшему общему) дуальных конусов: (⋃ i, f i).innerDualCone = ⨅ i, (f i).innerDualCone.
LaTeX
$$$\\Big(\\bigcup_i f(i)\\Big).innerDualCone = \\bigcap_i (f(i)).innerDualCone$$$
Lean4
@[deprecated ProperCone.innerDual_iUnion (since := "2025-07-06")]
theorem innerDualCone_iUnion {ι : Sort*} (f : ι → Set H) : (⋃ i, f i).innerDualCone = ⨅ i, (f i).innerDualCone :=
by
refine le_antisymm (le_iInf fun i x hx y hy => hx _ <| mem_iUnion_of_mem _ hy) ?_
intro x hx y hy
rw [ConvexCone.mem_iInf] at hx
obtain ⟨j, hj⟩ := mem_iUnion.mp hy
exact hx _ _ hj
