Documentation

Mathlib.Topology.Algebra.UniformFilterBasis

Uniform properties of neighborhood bases in topological algebra #

This files contains properties of filter bases on algebraic structures that also require the theory of uniform spaces.

The only result so far is a characterization of Cauchy filters in topological groups.

The uniform space structure associated to an abelian group filter basis via the associated topological abelian group structure.

Equations
Instances For

    The uniform space structure associated to an abelian group filter basis via the associated topological abelian group structure is compatible with its group structure.

    theorem AddGroupFilterBasis.cauchy_iff {G : Type u_1} [AddCommGroup G] (B : AddGroupFilterBasis G) {F : Filter G} :
    Cauchy F F.NeBot UB, MF, xM, yM, y - x U