English
Let X be a set with an equivalence relation R. Then two elements x and y are identified in the quotient X/R if and only if x is R-related to y.
Русский
Пусть X — множество с отношением эквивалентности R. Тогда два элемента x и y идентифицируются в фактор-множество X/R тогда и только тогда, когда xRi y.
LaTeX
$$$ [x] = [y] \iff r\,x\,y $$$
Lean4
@[simp]
theorem quot_mk_eq_iff {α : Type*} {r : α → α → Prop} (h : Equivalence r) (x y : α) :
Quot.mk r x = Quot.mk r y ↔ r x y := by
constructor
· rw [Quot.eq]
intro hxy
induction hxy with
| rel _ _ H => exact H
| refl _ => exact h.refl _
| symm _ _ _ H => exact h.symm H
| trans _ _ _ _ _ h₁₂ h₂₃ => exact h.trans h₁₂ h₂₃
· exact Quot.sound
