innerDualCone_sUnion — Mathlib

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]

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