setoid — Mathlib

English

The product α×α can be equipped with a Setoid structure whose equivalence relation is Rel α.

Русский

Произведение α×α можно снабдить структурой Setoid, эквивалентность которой задаётся Rel α.

LaTeX

$$$$ (\alpha \times \alpha, Rel\,\alpha) \text{ is a Setoid}. $$$$

Lean4

/-- One can use `attribute [local instance] Sym2.Rel.setoid` to temporarily
make `Quotient` functionality work for `α × α`. -/
def setoid (α : Type u) : Setoid (α × α) :=
  ⟨Rel α, Rel.is_equivalence⟩

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