instIsUniformGroupOfDiscreteUniformity

English

The discrete uniformity on a group makes it a uniform group; division is uniformly continuous under this uniformity.

Русский

Дискретная униформность на группе превращает её в равномерную группу; деление непрерывно по униформности.

LaTeX

$$$[UniformSpace G] [DiscreteUniformity G] : IsUniformGroup G$ with uniformContinuous_div.$$

Lean4

/-- The discrete uniformity makes a group a `IsUniformGroup. -/
@[to_additive /-- The discrete uniformity makes an additive group a `IsUniformAddGroup`. -/
    ]
instance [UniformSpace G] [DiscreteUniformity G] : IsUniformGroup G where
  uniformContinuous_div := DiscreteUniformity.uniformContinuous (G × G) fun p ↦ p.1 / p.2

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