innerDualCone_eq_iInter_innerDualCone_singleton

English

For any subset s, the dual cone s.innerDualCone is closed.

Русский

Для любого множества s двойственный конус s.innerDualCone замкнут.

LaTeX

$$$ IsClosed (s.innerDualCone) $$$

Lean4

/-- The dual cone of `s` equals the intersection of dual cones of the points in `s`. -/
@[deprecated "No replacement" (since := "2025-07-06")]
theorem innerDualCone_eq_iInter_innerDualCone_singleton :
    (s.innerDualCone : Set H) = ⋂ i : s, (({↑i} : Set H).innerDualCone : Set H) := by
  rw [← ConvexCone.coe_iInf, ← innerDualCone_iUnion, iUnion_of_singleton_coe]

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