isUniformAddGroup — Mathlib

English

Given an additive abelian group with a filter basis, the induced uniform structure makes it a uniform additive group.

Русский

Для абелевой группы с базисом фильтра, индуцированная униформность превращает её в равномерное аддитивное группу.

LaTeX

$$$IsUniformAddGroup(G)\text{ for }(G, B)\text{ with }B$-basis$$

Lean4

/-- The uniform space structure associated to an abelian group filter basis via the associated
topological abelian group structure is compatible with its group structure. -/
protected theorem isUniformAddGroup : @IsUniformAddGroup G B.uniformSpace _ :=
  @isUniformAddGroup_of_addCommGroup G _ B.topology B.isTopologicalAddGroup

Похожие утверждения