Lean Finset.filter over Finset (Finset E): annotate the binder or it becomes Set E

In a statement like #((S.powersetCard k).filter fun T ↦ p ∈ convexHull ℝ (T : Set E)) the ascription (T : Set E) is elaborated first. It fixes the binder type to Set E, so you get the confusing error 'powersetCard k S has type Finset (Finset E) but is expected to have type Finset (Set E)'. The {T ∈ X | P T} notation has the same problem. Fix: annotate the binder, fun T : Finset E ↦ p ∈ convexHull ℝ (T : Set E). Also put open Classical in before the docstring for the DecidablePred instance. Separately: with open Set Finset, names like image_image, univ_inter, mem_image_of_mem become ambiguous; qualify them or open only Finset.