comap — Mathlib

English

If f is a uniform inducing map of a group into a uniform group H, then the domain G acquires a uniform group structure.

Русский

Если отображение f является равномерно-индуктивным, то область G получает равномерную группу.

LaTeX

$$$\text{IsUniformInducing } f \Rightarrow IsUniformGroup G$.$$

Lean4

@[to_additive]
protected theorem comap {u : UniformSpace H} [IsUniformGroup H] [FunLike hom G H] [MonoidHomClass hom G H] (f : hom) :
    @IsUniformGroup G (u.comap f) _ :=
  letI : UniformSpace G := u.comap f;
  IsUniformInducing.isUniformGroup f ⟨rfl⟩

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