isQuotientMap_snd

Mathlib.Topology.Constructions.SumProd

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

English

The first projection is a quotient map provided Y is nonempty.

Русский

Первая проекция является факторным отображением при непустом Y.

LaTeX

$$$$[\text{Nonempty } Y] \Rightarrow \text{IsQuotientMap}(\mathrm{Prod.fst}).$$$$

Lean4

theorem isQuotientMap_snd [Nonempty X] : IsQuotientMap (Prod.snd : X × Y → Y) :=
  isOpenMap_snd.isQuotientMap continuous_snd Prod.snd_surjective

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

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

Разделы

Аффилиация

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