English
Let s : ι → Set α be an indexed partition of α. The quotient hs.Quotient is the quotient of α by the equivalence relation x ∼ y defined by x and y lying in the same part s(i) for some i. The projection map hs.proj : α → hs.Quotient sends every element to its equivalence class.
Русский
Пусть s : ι → Set α задаёт индексированное разбиение α. Фактор-пространство hs.Quotient является фактором α по эквивалентности x ∼ y, если x и y принадлежат одной части s(i) для некоторого i. Отображение hs.proj : α → hs.Quotient отправляет каждый элемент в его класс эквивалентности.
LaTeX
$$$ hs.Quotient \cong \alpha / \sim , \quad x \sim y \iff \exists i\, (x \in s(i) \land y \in s(i)). $$$
Lean4
/-- The quotient associated to an indexed partition. -/
protected def Quotient :=
Quotient hs.setoid
