proj — Mathlib

English

The projection map proj: α → hs.Quotient assigns to each x its equivalence class in the quotient by the indexed partition s.

Русский

Проекция proj: α → hs.Quotient отправляет каждый элемент x в его класс эквивалентности в фактор-пространстве, полученном из разбиения s.

LaTeX

$$$\operatorname{proj}(x) = [x] \in hs.Quotient$$$

Lean4

/-- The projection onto the quotient associated to an indexed partition. -/
def proj : α → hs.Quotient :=
  Quotient.mk''

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