isUniformGroup — Mathlib

English

If H is a uniform group and f: G → H is a monoid hom, then the comap uniform space on G via f makes G a uniform group.

Русский

Если H — равномерная группа, а f: G→H — гомоморфизм моноидов, то структура comap на G образует равномерную группу.

LaTeX

$$$\text{comap } f: IsUniformGroup\ G \to \text{ IsUniformGroup } (u.comap f).$$$

Lean4

@[to_additive]
theorem isUniformGroup [UniformSpace G] [UniformSpace H] [IsUniformGroup H] [FunLike hom G H] [MonoidHomClass hom G H]
    (f : hom) (hf : IsUniformInducing f) : IsUniformGroup G where
  uniformContinuous_div := by
    simp_rw [hf.uniformContinuous_iff, Function.comp_def, map_div]
    exact uniformContinuous_div.comp (hf.uniformContinuous.prodMap hf.uniformContinuous)

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