isQuotientMap

Mathlib.Topology.Covering

URI: https://scilib.ai/kg/mathlib#IsCoveringMap.isQuotientMap

English

If f is a covering map and surjective, then f is a quotient map.

Русский

Если покровное отображение сюръективно, то оно является образующей (quotient) картой.

LaTeX

$$$\IsCoveringMap(f) \Rightarrow (\text{Surjective}(f) \Rightarrow \text{IsQuotientMap}(f))$$$

Lean4

theorem isQuotientMap (hf' : Function.Surjective f) : IsQuotientMap f :=
  hf.isOpenMap.isQuotientMap hf.continuous hf'

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

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

Разделы

Аффилиация

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