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.

def AddGroupFilterBasis.uniformSpace {G : Type u_1} [AddCommGroup G] (B : AddGroupFilterBasis G) : UniformSpace G

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

Equations

• AddGroupFilterBasis.uniformSpace B = TopologicalAddGroup.toUniformSpace G

theorem AddGroupFilterBasis.uniformAddGroup {G : Type u_1} [AddCommGroup G] (B : AddGroupFilterBasis G) : UniformAddGroup 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.

theorem AddGroupFilterBasis.cauchy_iff {G : Type u_1} [AddCommGroup G] (B : AddGroupFilterBasis G) {F : Filter G} : Cauchy F ↔ Filter.NeBot F ∧ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U