ext — Mathlib

English

If two uniform group structures u and v on the same group G have the same nhds at 1, then u = v.

Русский

Если две униформные группы структуры u и v на одной группе G имеют одинаковые nhds в 1, то u = v.

LaTeX

$$$\\text{IsUniformGroup}(G) \\to \\text{IsUniformGroup}(G) \\to (\\nhds_{u}(1) = \\nhds_{v}(1) \\Rightarrow u = v)$$$

Lean4

@[to_additive]
theorem ext {G : Type*} [Group G] {u v : UniformSpace G} (hu : @IsUniformGroup G u _) (hv : @IsUniformGroup G v _)
    (h : @nhds _ u.toTopologicalSpace 1 = @nhds _ v.toTopologicalSpace 1) : u = v :=
  UniformSpace.ext <| by rw [@uniformity_eq_comap_nhds_one _ u _ hu, @uniformity_eq_comap_nhds_one _ v _ hv, h]

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