instFinalOppositeDiscreteQuotientCarrierToTopTotallyDisconnectedSpaceCostructuredArrowFintypeCatProfiniteOpToProfiniteOpPtAsLimitConeFunctorOp

English

There is a canonical Final object structure for the opposite of Profinite-related Extend constructions, establishing a finality property for the functorOp in an opposite setting.

Русский

Существуeт каноническая структура финала для противоположного объединения Profinite, устанавливающая свойство финальности для functorOp в противоположном контексте.

LaTeX

$$$\\text{Final}\\; (\\mathrm{Profinite}.Extend.\\mathrm{functorOp}\\; S.\\mathrm{asLimitCone})$$$

Lean4

instance : Final <| Profinite.Extend.functorOp S.asLimitCone :=
  Profinite.Extend.functorOp_final S.asLimitCone S.asLimit

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