mk' — Mathlib

English

A uniform group can be constructed by providing uniform continuity of multiplication and inversion; then the group is a uniform group.

Русский

Из задействования равномерной непрерывности умножения и обращения следует построение равномерной группы.

LaTeX

$$$\text{IsUniformGroup.mk'}(h_1,h_2) : IsUniformGroup G$ with appropriate uniform continuity assumptions.$$

Lean4

@[to_additive]
theorem mk' {α} [UniformSpace α] [Group α] (h₁ : UniformContinuous fun p : α × α => p.1 * p.2)
    (h₂ : UniformContinuous fun p : α => p⁻¹) : IsUniformGroup α :=
  ⟨by simpa only [div_eq_mul_inv] using h₁.comp (uniformContinuous_fst.prodMk (h₂.comp uniformContinuous_snd))⟩

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