proposition: Lemma ker_convex: is_convex_set (preimage f [set 0]).
proof: Proof. apply/asboolP=>x y p /= fx0 fy0. by rewrite linearD 2!linearZZ fx0 fy0 2!GRing.scaler0 addr0. Qed.
imports: mathcomp(all_ssreflect all_algebra vector reals ereal classical_sets boolp Rstruct) infotheo(convex Reals_ext) preliminaries Reals