instIsEquivEquiv — Mathlib

English

For any Setoid α, the relation ≈ on α is an equivalence relation. Specifically, reflexivity, symmetry, and transitivity hold for ≈.

Русский

Для любого множества эквивалентности α отношение ≈ является эквалентной связью; выполняются рефлексивность, симметричность и транзитивность.

LaTeX

$$$\\text{IsEquiv}(\\alpha, \\approx)$$$

Lean4

instance {α : Type*} [Setoid α] : IsEquiv α (· ≈ ·)
    where
  refl := Setoid.refl
  symm _ _ := Setoid.symm
  trans _ _ _ := Setoid.trans

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