mathlib documentation

topology.algebra.uniform_filter_basis

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.

@[protected]

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

Equations
@[protected]

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 add_group_filter_basis.cauchy_iff {G : Type u_1} [add_comm_group G] (B : add_group_filter_basis G) {F : filter G} :
cauchy F F.ne_bot ∀ (U : set G), U B(∃ (M : set G) (H : M F), ∀ (x y : G), x My My - x U)