isQuotientMap_projIcc

Mathlib.Topology.Order.ProjIcc

URI: https://scilib.ai/kg/mathlib#isQuotientMap_projIcc

← MathLib Explorer

English

The map projIcc is a quotient map.

Русский

Карта projIcc является факторной картой (quotient map).

LaTeX

$$$\\text{IsQuotientMap}(\\text{projIcc } a b h).$$$

Lean4

theorem isQuotientMap_projIcc : IsQuotientMap (projIcc a b h) :=
  isQuotientMap_iff.2
    ⟨projIcc_surjective h, fun s => ⟨fun hs => hs.preimage continuous_projIcc, fun hs => ⟨_, hs, by ext; simp⟩⟩⟩

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

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

Разделы

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

Аффилиация

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