mk''_rightQuotientEquiv — Mathlib

English

For any hT, q, the equality Quotient.mk'' (rightQuotientEquiv hT q) = q holds, expressing compatibility of the representative map with the quotient structure.

Русский

Для любого hT, q верно: Quotient.mk'' (rightQuotientEquiv hT q) = q, что выражает совместимость отображения выборочного представителя с фактор-структурой.

LaTeX

$$$\\text{Quotient.mk''}(\\text{rightQuotientEquiv}(hT)\, q) = q$$$

Lean4

@[to_additive]
theorem mk''_rightQuotientEquiv (hT : IsComplement H T) (q : Quotient (QuotientGroup.rightRel H)) :
    Quotient.mk'' (rightQuotientEquiv hT q : G) = q :=
  (rightQuotientEquiv hT).symm_apply_apply q

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