continuous_lift

Mathlib.Topology.Separation.Hausdorff

URI: https://scilib.ai/kg/mathlib#T2Quotient.continuous_lift

← MathLib Explorer

English

The lift map T2Quotient.lift hf is continuous for hf : Continuous f.

Русский

Отображение lift непрерывно при hf : Continuous f.

LaTeX

$$$ Continuous(T2Quotient.lift\\ hf)$$$

Lean4

theorem continuous_lift {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y] [T2Space Y] {f : X → Y}
    (hf : Continuous f) : Continuous (T2Quotient.lift hf) :=
  continuous_coinduced_dom.mpr hf

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

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

Разделы

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

Аффилиация

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