proposition: Lemma pseudometric_normal {R : realType} {X : pseudoMetricType R} : normal_space X.
proof: Proof. apply/normal_openP => A B clA clB AB0. have eps' (D : set X) : closed D -> forall x, exists eps : {posnum R}, ~ D x -> ball x eps%:num `&` D = set0. move=> clD x; have [nDx|?] := pselect (~ D x); last by exists 1%:pos. have /regular_openP/(_ _ clD) [//|] := @uniform_regular X x. move=> U [V] [+ oV] Ux /subsetC BV /disjoints_subset UV0. rewrite openE /interior => /(_ _ Ux); rewrite -nbhs_ballE => -[]. move => _/posnumP[eps] beU; exists eps => _; apply/disjoints_subset. exact: (subset_trans beU (subset_trans UV0 _)). pose epsA x := projT1 (cid (eps' _ clB x)). pose epsB x := projT1 (cid (eps' _ clA x)). exists (\bigcup_(x in A) interior (ball x ((epsA x)%:num / 2)%:pos%:num)). exists (\bigcup_(x in B) interior (ball x ((epsB x)%:num / 2)%:pos%:num)). split. - by apply: bigcup_open => ? ?; exact: open_interior. - by apply: bigcup_open => ? ?; exact: open_interior. - by move=> x ?; exists x => //; exact: nbhsx_ballx. - by move=> y ?; exists y => //; exact: nbhsx_ballx. - apply/eqP/negPn/negP/set0P => -[z [[x Ax /interior_subset Axe]]]. case=> y By /interior_subset Bye; have nAy : ~ A y. by move: AB0; rewrite setIC => /disjoints_subset; exact. have nBx : ~ B x by move/disjoints_subset: AB0; exact. have [|/ltW] := leP ((epsA x)%:num / 2) ((epsB y)%:num / 2). move/ball_sym: Axe => /[swap] /le_ball /[apply] /(ball_triangle Bye). rewrite -splitr => byx; have := projT2 (cid (eps' _ clA y)) nAy. by rewrite -subset0; apply; split; [exact: byx|]. move/ball_sym: Bye =>/[swap] /le_ball /[apply] /(ball_triangle Axe). rewrite -splitr => byx; have := projT2 (cid (eps' _ clB x)) nBx. by rewrite -subset0; apply; split; [exact: byx|]. 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