fact: Definition supporting_hyperplane (A : set E) (f: {linear E -> R^o}) (a: R_ringType) := (exists x, x \in A /\ f x = a) /\ ((forall x, x \in A -> f x <= a) \/ (forall x, x \in A -> a <= f x)).
imports: mathcomp(all_ssreflect all_algebra vector reals ereal classical_sets boolp Rstruct) infotheo(convex Reals_ext) preliminaries Reals