eq — Mathlib · SciLib

English

Two elements are identified in the quotient precisely when the representative x is related to y by the Setoid relation: Quot.mk r x = ⟦y⟧ iff r x y.

Русский

В квоте два представителя идентифицируются тогда и только тогда, когда x и y эквивалентны по r: Quot.mk r x = ⟦y⟧ ⇔ r x y.

LaTeX

$$$\\Quotient.mk r x = \\overline{y} \\;\\iff\\; r\\,x\,y$$$

Lean4

@[simp]
theorem eq {r : Setoid α} {x y : α} : Quotient.mk r x = ⟦y⟧ ↔ r x y :=
  ⟨Quotient.exact, Quotient.sound⟩

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