instTopologicalSpaceAutFunctorFintypeCat

English

The topology on Aut F is induced by the embedding autEmbedding(F).

Русский

Топология на Aut F индуцирована встраиванием autEmbedding(F).

LaTeX

$$$\\text{TopologicalSpace}(Aut F)=\\operatorname{induced}(autEmbedding(F),\\; \\text{?})$$$

Lean4

/-- `Aut F` is equipped with the by the embedding into `∀ X, Aut (F.obj X)` induced embedding. -/
instance : TopologicalSpace (Aut F) :=
  TopologicalSpace.induced (autEmbedding F) inferInstance

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