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 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 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 ``` ### 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) ``` ## Closed balls ``` closed_ball_ norm x e := [set y | norm (x - y) <= e] closed_ball == closure of a ball ```