proposition: Lemma closed_disjoint_closed_ball {R : realFieldType} {M : normedModType R} (K : set M) z : closed K -> ~ K z -> \forall d \near 0^'+, closed_ball z d `&` K = set0.
proof: Proof. rewrite -openC => /open_subball /[apply]; move=> [e /= e0]. move=> /(_ (e / 2)) /= ; rewrite sub0r normrN gtr0_norm ?divr_gt0//. rewrite ltr_pdivrMr// ltr_pMr// ltr1n => /(_ erefl isT). move/subsets_disjoint; rewrite setCK => ze2K0. exists (e / 2); first by rewrite /= divr_gt0. move=> x /= + x0; rewrite sub0r normrN gtr0_norm// => xe. by move: ze2K0; apply: subsetI_eq0 => //=; exact: closed_ball_subset. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrint ssrnum finmap matrix) mathcomp(rat interval zmodp vector fieldext falgebra) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality set_interval Rstruct) ereal reals signed topology prodnormedzmodule