toUnits_homeomorph — Mathlib

English

If G is a group with a topological inverse, then G is homeomorphic to its units Gˣ.

Русский

Если G — группа с топологическим взятием обратного, то G гомеоморфна своей группе единиц Gˣ.

LaTeX

$$$ G \\cong_{top} G^{\\times} $$$

Lean4

/-- If `G` is a group with topological `⁻¹`, then it is homeomorphic to its units. -/
@[to_additive /-- If `G` is an additive group with topological negation, then it is homeomorphic to
    its additive units. -/
    ]
def toUnits_homeomorph [Group G] [TopologicalSpace G] [ContinuousInv G] : G ≃ₜ Gˣ
    where
  toEquiv := toUnits.toEquiv
  continuous_toFun := Units.continuous_iff.2 ⟨continuous_id, continuous_inv⟩
  continuous_invFun := Units.continuous_val

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