proj

Mathlib.Topology.DiscreteQuotient

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

English

Let π: X → X/∼ be the natural projection sending x to its equivalence class [x].

Русский

Пусть \\pi: X → X/∼ — естественная проекция, отправляющая x в свой класс эквивалентности [x].

LaTeX

$$$ \\pi: X \\to X/\\sim, \\quad \\pi(x) = [x] $$$

Lean4

/-- The projection from `X` to the given discrete quotient. -/
def proj : X → S :=
  Quotient.mk''

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

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

Разделы

Аффилиация

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