Uniform properties of neighborhood bases in topological algebra #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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]

def add_group_filter_basis.uniform_space {G : Type u_1} [add_comm_group G] (B : add_group_filter_basis G) :

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

Equations

B.uniform_space = topological_add_group.to_uniform_space G

source

@[protected]

theorem add_group_filter_basis.uniform_add_group {G : Type u_1} [add_comm_group G] (B : add_group_filter_basis G) :

uniform_add_group G

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

source

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 : G), x ∈ M → ∀ (y : G), y ∈ M → y - x ∈ U)