proposition: Lemma ereal_hausdorff : hausdorff_space (\bar R).
proof: Proof. move=> -[r| |] // [r' | |] //=. - move=> rr'; congr (_%:E); apply Rhausdorff => /= A B rA r'B. have [/= z [[r0 ? r0z] [r1 ?]]] := rr' _ _ (nbhs_image_EFin rA) (nbhs_image_EFin r'B). by rewrite -r0z => -[r1r0]; exists r0; split => //; rewrite -r1r0. - have /(@nbhs_open_ereal_lt _ (fun x => x + 1)) loc_r : r < r + 1. by rewrite ltrDl. move/(_ _ _ loc_r (nbhs_open_ereal_pinfty (r + 1))) => -[z [zr rz]]. by move: (lt_trans rz zr); rewrite lte_fin ltxx. - have /(@nbhs_open_ereal_gt _ (fun x => x - 1)) loc_r : r - 1 < r. by rewrite ltrBlDr ltrDl. move/(_ _ _ loc_r (nbhs_open_ereal_ninfty (r - 1))) => -[z [rz zr]]. by move: (lt_trans zr rz); rewrite ltxx. - have /(@nbhs_open_ereal_lt _ (fun x => x + 1)) loc_r' : r' < r' + 1. by rewrite ltrDl. move/(_ _ _ (nbhs_open_ereal_pinfty (r' + 1)) loc_r') => -[z [r'z zr']]. by move: (lt_trans zr' r'z); rewrite ltxx. - move/(_ _ _ (nbhs_open_ereal_pinfty 0) (nbhs_open_ereal_ninfty 0)). by move=> -[z [zx xz]]; move: (lt_trans xz zx); rewrite ltxx. - have /(@nbhs_open_ereal_gt _ (fun x => x - 1)) yB : r' - 1 < r'. by rewrite ltrBlDr ltrDl. move/(_ _ _ (nbhs_open_ereal_ninfty (r' - 1)) yB) => -[z [zr' r'z]]. by move: (lt_trans r'z zr'); rewrite ltxx. - move/(_ _ _ (nbhs_open_ereal_ninfty 0) (nbhs_open_ereal_pinfty 0)). by move=> -[z [zO Oz]]; move: (lt_trans Oz zO); rewrite ltxx. 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