(V : G →L[ℂ] E) (X : E →L[ℂ] E) (hViso : ∀ x : G, ‖V x‖ = ‖x‖) (S : Set ℂ) (hconv : Convex ℝ S) (hS : numRange X ⊆ S) : convexHull ℝ (numRange (compress V X)) ⊆ S

Initializing...

(V : G →L[ℂ] E) (X : E →L[ℂ] E) (hViso : ∀ x : G, ‖V x‖ = ‖x‖) (S : Set ℂ) (hconv : Convex ℝ S) (hS : numRange X ⊆ S) : convexHull ℝ (numRange (compress V X)) ⊆ S · Prove2Me