quotientEquivClasses_mk_eq — Mathlib

English

The image of the equivalence class of a under the quotientEquivClasses map equals the set of elements related to a.

Русский

Образ эквивалентного класса a при отображении quotientEquivClasses равен множеству элементов, эквивалентных a.

LaTeX

$$$ (quotientEquivClasses\\ r\\ (Quotient.mk\\ r\\ a) : Set \\alpha) = \\{ x \\mid r\\ x\\ a \\}$$$

Lean4

@[simp]
theorem quotientEquivClasses_mk_eq (r : Setoid α) (a : α) :
    (quotientEquivClasses r (Quotient.mk r a) : Set α) = {x | r x a} :=
  (@Subtype.ext_iff _ _ _ ⟨{x | r x a}, Setoid.mem_classes r a⟩).mp rfl

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