no goals
𝕜 : Type u_2
E : Type u_3
F : Type ?u.9687
G : Type ?u.9690
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
S T : ConvexCone 𝕜 E
ι : Sort u_1
f : ι → ConvexCone 𝕜 E
⊢ ↑(iInf f) = ⋂ (i : ι), ↑(f i)
simp [iInf]