quotientEquivOfIsCompl_apply_mk_coe

English

The application of quotientEquivOfIsCompl to a quotient element mk x recovers the original element x when mapped back through mk.

Русский

Применение quotientEquivOfIsCompl к элементу mk x восстанавливает исходный x при обратном отображении через mk.

LaTeX

$$$quotientEquivOfIsCompl p q h \\; (Quotient.mk x) = x$$$

Lean4

@[simp]
theorem quotientEquivOfIsCompl_apply_mk_coe (h : IsCompl p q) (x : q) :
    quotientEquivOfIsCompl p q h (Quotient.mk x) = x :=
  (quotientEquivOfIsCompl p q h).apply_symm_apply x

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