ext_iff — Mathlib

English

For a group G and uniform structures u,v, IsUniformGroup G holds; then u = v if and only if nhds(1) under u equals nhds(1) under v.

Русский

Для группы G и униформных структур u, v, IsUniformGroup G эквивалентно: u = v тогда и только тогда, когда nhds(1) по u равно nhds(1) по v.

LaTeX

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

Lean4

@[to_additive]
theorem ext_iff {G : Type*} [Group G] {u v : UniformSpace G} (hu : @IsUniformGroup G u _) (hv : @IsUniformGroup G v _) :
    u = v ↔ @nhds _ u.toTopologicalSpace 1 = @nhds _ v.toTopologicalSpace 1 :=
  ⟨fun h => h ▸ rfl, hu.ext hv⟩

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