instTopologicalSpaceCarrierObjFintypeCat

Mathlib.CategoryTheory.Galois.Topology

URI: https://scilib.ai/kg/mathlib#CategoryTheory.PreGaloisCategory.instTopologicalSpaceCarrierObjFintypeCat

English

The topology on Aut(F.obj X) is the discrete topology for every X.

Русский

Топология на Aut(F.obj X) — дискретная для каждого X.

LaTeX

$$$\\text{The topology on }Aut(F.obj X)\\text{ is discrete for all }X$$$

Lean4

/-- We put the discrete topology on `F.obj X`. -/
scoped instance (X : C) : TopologicalSpace (F.obj X) :=
  ⊥

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru