ofSetoid — Mathlib

English

If we apply the setoid partition to the whole universe univ, the membership condition reduces to s a b.

Русский

Если рассматривать разбиение множества по всему множеству (univ), то условие членства сокращается до s a b.

LaTeX

$$$ b \\in (ofSetoid(s)).part(a) \\iff s(a,b) $$

Lean4

/-- A setoid over a finite type induces a finpartition of the type's elements,
where the parts are the setoid's equivalence classes. -/
@[simps! -isSimp]
def ofSetoid (s : Setoid α) [DecidableRel s.r] : Finpartition (univ : Finset α) :=
  ofSetSetoid s univ

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