ext_iff — Mathlib

English

IsTopologicalGroup structure on G is determined by nhds at 1; two structures are equal iff their nhds at 1 coincide.

Русский

Структура IsTopologicalGroup на G определяется через nhds в единице; равенство структур эквивалентно совпадению nhds(1).

LaTeX

$$$IsTopologicalGroup\;ext\_iff$$$

Lean4

@[to_additive]
theorem ext_iff {G : Type*} [Group G] {t t' : TopologicalSpace G} (tg : @IsTopologicalGroup G t _)
    (tg' : @IsTopologicalGroup G t' _) : t = t' ↔ @nhds G t 1 = @nhds G t' 1 :=
  ⟨fun h => h ▸ rfl, tg.ext tg'⟩

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