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