of_compactSpace — Mathlib

English

If a group is equipped with a compact topology and has a continuous division, then it carries a uniform group structure; in particular the division map is uniformly continuous.

Русский

Если группа имеет компактное верхнее полупространство и операция деления непрерывна, то она может быть сведена к равномерной групповой структуре; в частности отображение деления является равномерно непрерывным.

LaTeX

$$$\text{CompactSpace } G \land \text{Group } G \land \text{ContinuousDiv } G \Rightarrow \text{IsUniformGroup } G.$$$

Lean4

@[to_additive]
instance of_compactSpace [UniformSpace β] [Group β] [ContinuousDiv β] [CompactSpace β] : IsUniformGroup β where
  uniformContinuous_div := CompactSpace.uniformContinuous_of_continuous continuous_div'

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