classes — Mathlib

English

For a setoid r on α, the collection of its equivalence classes is the set { { x ∈ α : r(x,y) } : y ∈ α }, i.e. the family of blocks determined by r.

Русский

Для множества эквивалентности r на α множество эквивалентных классов равно { { x ∈ α : r(x,y) } : y ∈ α }, т. е. семейство блоков, определяемых r.

LaTeX

$$$\\operatorname{classes}(r) = \\{ \\{ x \\in α : r(x,y) \\} : y \\in α \\}.$$$

Lean4

/-- Makes the equivalence classes of an equivalence relation. -/
def classes (r : Setoid α) : Set (Set α) :=
  {s | ∃ y, s = {x | r x y}}

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