toTopologicalSpace_injective — Mathlib

English

The map toTopologicalSpace from GroupTopology α to TopologicalSpace α is injective.

Русский

Отображение toTopologicalSpace: GroupTopology α → TopologicalSpace α инъективно.

LaTeX

$$$\\mathrm{Injective}\\bigl(\\text{toTopologicalSpace} : \\mathrm{GroupTopology}(\\alpha) \\to \\mathrm{TopologicalSpace}(\\alpha)\\bigr)$$$

Lean4

@[to_additive]
theorem toTopologicalSpace_injective : Function.Injective (toTopologicalSpace : GroupTopology α → TopologicalSpace α) :=
  fun f g h => by
  cases f
  cases g
  congr

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