instSetoid — Mathlib

English

AbsoluteValue objects form a Setoid with IsEquiv as the equivalence relation, with reflexivity, symmetry and transitivity.

Русский

Объекты модуля абсолютной величины образуют множество-эквивалентность с отношением эквивалентности IsEquiv, удовлетворяющим рефлексивности, симметрии и транзитивности.

LaTeX

$$$\\text{Setoid}(\\text{AbsoluteValue}(R,S))$ with $v\\sim w$ iff $v.IsEquiv w$$$

Lean4

instance : Setoid (AbsoluteValue R S) where
  r := IsEquiv
  iseqv :=
    { refl := .refl
      symm := .symm
      trans := .trans }

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