Separation of points from open convex sets by heights

In a real Hilbert space, a point outside a nonempty open convex set W is strictly separated from W by a continuous linear functional (geometric_hahn_banach_open_point). By the Riesz representation, such a functional is a positive multiple of the height x ↦ ⟪u, x⟫ along a unit vector u. Hence a set whose heights along every unit vector are heights of points of W is contained in W.

Main results

• Convex.subset_of_image_inner_subset: a set whose heights along every unit vector are heights of points of a nonempty open convex set W is contained in W.

theorem Convex.subset_of_image_inner_subset {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {U W : Set E} (hW : Convex ℝ W) (hWo : IsOpen W) (hWn : W.Nonempty) (hUW : ∀ (u : E), ‖u‖ = 1 → (fun (x : E) => inner ℝ u x) '' U ⊆ (fun (x : E) => inner ℝ u x) '' W) : U ⊆ W

Containment in an open convex set from directional images. If the heights ⟪u, x⟫ of the points of U along every unit vector u are heights of points of a nonempty open convex set W, then U ⊆ W: a point outside W is strictly separated from it by a continuous linear functional, which is a positive multiple of the height along a unit vector.