no goals
𝕜 : Type ?u.19025
E : Type ?u.19028
F : Type ?u.19031
G : Type ?u.19034
H : Type u_1
inst✝¹ : NormedAddCommGroup H
inst✝ : InnerProductSpace ℝ H
s t : Set H
⊢ ↑(innerDualCone s) = ⋂ (i : ↑s), ↑(innerDualCone {↑i})
rw [← ConvexCone.coe_iInf, ← innerDualCone_iUnion, iUnion_of_singleton_coe]