Module mathcomp.analysis.topology_theory.pseudometric_structure

# PseudoMetric Spaces This file provides pseudometric spaces, complete pseudometric spaces, and the corresponding theory. Note that a classic metric space is simply pseudometric + hausdorff. However we will make extensive use of the of the non-hausdorff case, such as in our proof of Urysohn's lemma. ## Mathematical structures ### PseudoMetrics ``` entourage_ ball == entourages defined using balls pseudoMetricType == interface type for pseudo metric space structure: a type equipped with balls The HB class is PseudoMetric. pseudoPMetricType == a pointed pseudoMetric space discrete_topology dscT == the discrete topology on T, provided dscT : discrete_space T ball x e == ball of center x and radius e nbhs_ball_ ball == nbhs defined using the given balls nbhs_ball == nbhs defined using balls in a pseudometric space discrete_ent == entourages of the discrete uniformity topology discrete_ball == singleton balls for the discrete metric discrete_topology_type == equip choice types with a discrete topology ``` `discrete_ent` is equipped with the `Uniform` structure. ### Factories ``` Nbhs_isPseudoMetric == factory to build a topological space from a mixin for a pseudoMetric space ``` ### Complete Pseudometrics ``` ball_ N == balls defined by the norm/absolute value N completePseudoMetricType == interface type for a complete pseudometric space structure The HB class is CompletePseudoMetric. cauchy_ex F <-> the set of sets F is a cauchy filter (epsilon-delta definition) cauchy_ball F <-> the set of sets F is a cauchy filter (using the near notations) ```