Module mathcomp.analysis.separation_axioms

# Separation Axioms This file introduces the separation axioms, a series of topological properties about separating points and sets. They are somtimes denoted by the names T0 through T6. Although we use their full names (hausdorff, accessible, uniform, etc). This file also provides related topological properties like zero dimensional and perfect, and discrete. ``` set_nbhs A == filter from open sets containing A ``` ## The classic separation axioms ``` kolmogorov_space T == T is a Kolmogorov space (T0) accessible_space T == T is an accessible space (T1) hausdorff_space T == T is a Hausdorff space (T2) close x y == x and y are arbitrarily close w.r.t. open sets normal_space T == T is normal (sometimes called T4) regular_space T == T is regular (sometimes called T3) ``` ## related concepts ``` totally_disconnected A == the only connected subsets of A are empty or singletons zero_dimensional T == points are separable by a clopen set perfect_set A == A is closed, and every point in A is a limit point of A ``` ## metrizability for uniform spaces ``` countable_uniform.type == endows a pseudoMetric on a uniform type whose entourage has a countable basis sup_pseudometric == the pseudometric induced for the supremum of countably many pseudoMetrics gauge E == for an entourage E, gauge E is a filter which includes `iter n split_ent E`. Critically, `gauge E` forms a uniform space with a countable uniformity. perfect_set A := closed A /\ limit_point A = A ```