instT2SpaceAutFunctorFintypeCat

Mathlib.CategoryTheory.Galois.Topology

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

English

Aut F is a Hausdorff space under the induced topology.

Русский

Aut F является хаусдорфовым пространством в индуцированной топологии.

LaTeX

$$$\text{Hausdorff}(\operatorname{Aut} F)$$$

Lean4

instance : T2Space (Aut F) :=
  T2Space.of_injective_continuous (autEmbedding_injective F) continuous_induced_dom

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

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

Разделы

Аффилиация

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