continuous_mk

Mathlib.Topology.Separation.Hausdorff

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

English

As above: inductionOn principle for T2Quotient.

Русский

Как выше: принцип индукции по T2Quotient.

LaTeX

$$$ \\forall q:\\, T2Quotient X,\n(\\forall x:X, P( T2Quotient.mk\\ x)) \\Rightarrow P(q)$$$

Lean4

theorem continuous_mk : Continuous (mk : X → T2Quotient X) :=
  continuous_quotient_mk'

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

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

Разделы

Аффилиация

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