proposition: Lemma pseudoMetricNormedZModType_hausdorff (R : realFieldType) (V : pseudoMetricNormedZmodType R) : hausdorff_space V.
proof: Proof. move=> p q clp_q; apply/subr0_eq/normr0_eq0/Rhausdorff => A B pq_A. rewrite -(@normr0 _ V) -(subrr p) => pp_B. suff loc_preim r C : nbhs`|p - r| C -> nbhs r ((fun r => `|p - r|) @^-1` C). have [r []] := clp_q _ _ (loc_preim _ _ pp_B) (loc_preim _ _ pq_A). by exists `|p - r|. move=> [e egt0 pre_C]; apply: nbhs_le_nbhs_norm; exists e => //= s /= rse. apply: pre_C; apply: le_lt_trans (ler_dist_dist _ _) _. by rewrite opprB addrC subrKA distrC. 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