Module mathcomp.analysis.topology_theory.uniform_structure

# Uniform Spaces This file provides uniform spaces, and their theory. It also includes complete spaces, which extends uniform in the hierarchy. ## Mathematical structures ### Uniform ``` nbhs_ ent == neighborhoods defined using entourages uniformType == interface type for uniform spaces: a type equipped with entourages The HB class is Uniform. puniformType == a pointed and uniform space entourage == set of entourages in a uniform space split_ent E == when E is an entourage, split_ent E is an entourage E' such that E' \o E' is included in E when seen as a relation countable_uniformity T == T's entourage has a countable base This is equivalent to `T` being metrizable. unif_continuous f == f is uniformly continuous entourage_ ball == entourages defined using balls ``` ## Factories ``` Nbhs_isUniform == factory to build a topological space from a mixin for a uniform space ``` ### Complete uniform spaces ``` cauchy F <-> the set of sets F is a cauchy filter (entourage definition) completeType == interface type for a complete uniform space structure The HB class is Complete. ```