out_eq' — Mathlib

English

There is a canonical representative operator such that applying mk to the representative of a coset returns the coset itself.

Русский

Существует канонический выбор представителя косета: образ mk представителя косета возвращает сам косет.

LaTeX

$$$\text{mk}(\text{out}(a)) = a$ for every $a$ in the quotient $\alpha / s$$$

Lean4

@[to_additive]
theorem out_eq' (a : α ⧸ s) : mk a.out = a :=
  Quotient.out_eq' a

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