instIsTopologicalGroupCarrierToTopTotallyDisconnectedSpacePtProfiniteLimitConeCompForget₂

English

The carrier of the limit cone point, viewed as a topological space, inherits a topological group structure (and the necessary axioms) from ProfiniteGrp.

Русский

Картеж предельной точки образует топологическую группу, наследующуюся от ProfiniteGrp.

LaTeX

$$$\text{IsTopologicalGroup}(\mathrm{limit\;Cone}(F).pt)$$$

Lean4

instance : IsTopologicalGroup (Profinite.limitCone (F ⋙ (forget₂ ProfiniteGrp Profinite))).pt :=
  inferInstanceAs (IsTopologicalGroup (limitConePtAux F))

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