English
If a topological group H admits a ContinuousMulEquiv with a profinite group G, then H is profinite (i.e., compact and totally disconnected) and obtains a ProfiniteGrp structure via this equivalence.
Русский
Пусть топологическая группа H эквивалентна по непрерывному умножению некоторой профинированной группе G; тогда H также профинирована, то есть компактна и частично раздроблена.
LaTeX
$$$(\exists e : G \simeq_{t*} H) \Rightarrow H \text{ is profinite for } G \text{ profinite}$$$
Lean4
/-- A topological group that has a `ContinuousMulEquiv` to a profinite group is profinite. -/
@[to_additive /-- A topological additive group that has a `ContinuousAddEquiv` to a
profinite additive group is profinite. -/
]
def ofContinuousMulEquiv {G : ProfiniteGrp.{u}} {H : Type v} [TopologicalSpace H] [Group H] [IsTopologicalGroup H]
(e : G ≃ₜ* H) : ProfiniteGrp.{v} :=
let _ : CompactSpace H := Homeomorph.compactSpace e.toHomeomorph
let _ : TotallyDisconnectedSpace H := Homeomorph.totallyDisconnectedSpace e.toHomeomorph
.of H
