proposition: Lemma norm_hausdorff : hausdorff_space V.
proof: Proof. rewrite ball_hausdorff => a b ab. have ab2 : 0 < `|a - b| / 2 by apply divr_gt0 => //; rewrite normr_gt0 subr_eq0. set r := PosNum ab2; exists (r, r) => /=. apply/negPn/negP => /set0P[c] []; rewrite -ball_normE /ball_ => acr bcr. have r22 : r%:num * 2 = r%:num + r%:num. by rewrite (_ : 2 = 1 + 1) // mulrDr mulr1. move: (ltrD acr bcr); rewrite -r22 (distrC b c). move/(le_lt_trans (ler_distD c a b)). by rewrite -mulrA mulVr ?mulr1 ?ltxx // unitfE. 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