rep_spec — Mathlib

English

Let q be a quotient of a type by a setoid s. Then the quotient class of a representative rep(q) equals q: ⟦q.rep⟧ = q.

Русский

Пусть q — фактор по отношению эквивалентности s. Тогда класс эквивалентности представителя q.rep равен q: ⟦q.rep⟧ = q.

LaTeX

$$$ ⟦q.{\\rm rep}\\vphantom{q} \\!\\!\\! \\! = q $$$

Lean4

theorem rep_spec (q : Quotient s) : ⟦q.rep⟧ = q :=
  choose_spec (exists_rep q)

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