instTotallyDisconnectedSpaceAutFunctorFintypeCat

Mathlib.CategoryTheory.Galois.Topology

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

← MathLib Explorer

English

Aut F is totally disconnected in the induced topology.

Русский

Aut F полностью разобщено в индуцированной топологии.

LaTeX

$$$\operatorname{TotallyDisconnectedSpace}(\operatorname{Aut} F)$$$

Lean4

instance : TotallyDisconnectedSpace (Aut F) :=
  (autEmbedding_isClosedEmbedding F).isEmbedding.isTotallyDisconnected_range.mp
    (isTotallyDisconnected_of_totallyDisconnectedSpace _)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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