fact: Definition ext (A : set E) := [set x | forall u v, u \in A -> v \in A -> x \in segment u v -> x = u \/ x = v]%classic.
imports: mathcomp(all_ssreflect all_algebra vector reals ereal classical_sets boolp Rstruct) infotheo(convex Reals_ext) preliminaries Reals