setoid — Mathlib

English

The equivalence relation associated to an indexed partition is the ker of the index map: two elements are equivalent if they have the same index.

Русский

Эталонная эквивалентность, связанная с индексированным разбиением, является ядром индекса: элементы эквивалентны тогда и только когда имеют одинаковый индекс.

LaTeX

$$$$ x \\sim y \\iff \\operatorname{index}(x) = \\operatorname{index}(y). $$$$

Lean4

/-- The equivalence relation associated to an indexed partition. Two
elements are equivalent if they belong to the same set of the partition. -/
protected abbrev setoid (hs : IndexedPartition s) : Setoid α :=
  Setoid.ker hs.index

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