proj_surjective

Mathlib.Topology.DiscreteQuotient

URI: https://scilib.ai/kg/mathlib#DiscreteQuotient.proj_surjective

English

The projection map π is surjective onto the quotient space.

Русский

Проекция $\\pi$ отображает X на каждый класс в X/~; она сюръективна.

LaTeX

$$$ \\forall y \\in X/\\sim\\; \\exists x \\in X: \\pi(x) = y $$$

Lean4

theorem proj_surjective : Function.Surjective S.proj :=
  Quotient.mk''_surjective

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

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

Разделы

Аффилиация

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