English
Let s be a subset of H. Then the dual cone of s equals the intersection over all i in s of the dual cone of the singleton {i}: s.innerDualCone = ⋂ i : s, ({i}.innerDualCone).
Русский
Пусть s ⊆ H. Тогда дуальный конус множества s равен пересечению по всем i∈s дуальных конусов одноэлементного множества {i}: s.innerDualCone = ⋂ i : s, ({i}.innerDualCone).
LaTeX
$$$ s.innerDualCone = \\bigcap_{i \\in s} (\\{i\\}.innerDualCone) $$$
Lean4
@[deprecated ProperCone.innerDual_sUnion (since := "2025-07-06")]
theorem innerDualCone_sUnion (S : Set (Set H)) : (⋃₀ S).innerDualCone = sInf (Set.innerDualCone '' S) := by
simp_rw [sInf_image, sUnion_eq_biUnion, innerDualCone_iUnion]