instIsUniformAddGroup — Mathlib

English

If R and M are uniform spaces with additive groups, then tsze R M is an uniform additive group.

Русский

Если R и M — равномерные пространства с аддитивной группой, то tsze R M образует равномерную группу сложения.

LaTeX

$$$\\operatorname{IsUniformAddGroup}(\\mathrm{tsze}(R,M))$$$

Lean4

instance [AddGroup R] [AddGroup M] [IsUniformAddGroup R] [IsUniformAddGroup M] : IsUniformAddGroup (tsze R M) :=
  inferInstanceAs <| IsUniformAddGroup (R × M)

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