ext — Mathlib

English

Given a bilinear-type ambient structure with hmul, hinv, hleft, hconj, one obtains an IsTopologicalGroup structure on G.

Русский

При заданной совместной структуре умножения, инверсии и сопряжения на группу G, образуется топологическая группа.

LaTeX

$$$IsTopologicalGroup.of\_nhds\_one(hmul)(hinv)(hleft)(hconj)$$$

Lean4

@[to_additive]
theorem ext {G : Type*} [Group G] {t t' : TopologicalSpace G} (tg : @IsTopologicalGroup G t _)
    (tg' : @IsTopologicalGroup G t' _) (h : @nhds G t 1 = @nhds G t' 1) : t = t' :=
  TopologicalSpace.ext_nhds fun x ↦ by
    rw [← @nhds_translation_mul_inv G t _ _ x, ← @nhds_translation_mul_inv G t' _ _ x, ← h]

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