discreteTopology_fiber

Mathlib.Topology.Covering

URI: https://scilib.ai/kg/mathlib#IsEvenlyCovered.discreteTopology_fiber

← MathLib Explorer

English

If x is evenly covered by f with fiber I, then f^{-1}({x}) carries the discrete topology.

Русский

Если x равномерно покрыт f с волокном I, то f^{-1}({x}) носит дискретную топологию.

LaTeX

$$$\\operatorname{DiscreteTopology}(f^{-1}({x}))$$$

Lean4

theorem discreteTopology_fiber {x : X} (h : IsEvenlyCovered f x I) : DiscreteTopology (f ⁻¹' { x }) :=
  have := h.1;
  h.fiberHomeomorph.discreteTopology

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

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

Разделы

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

Аффилиация

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