rightQuotientEquiv_apply — Mathlib

English

There is a form of evaluation for the right quotient equivalence: given a suitable hf, the value equals f(q).

Русский

Существуют правила вычисления для правой эквив: при заданном hf значение равно f(q).

LaTeX

$$$\\forall f, hf, q:\\; (rightQuotientEquiv (isComplement_range_right hf) q : G) = f q$$$

Lean4

@[to_additive]
theorem rightQuotientEquiv_apply {f : Quotient (QuotientGroup.rightRel H) → G} (hf : ∀ q, Quotient.mk'' (f q) = q)
    (q : Quotient (QuotientGroup.rightRel H)) : (rightQuotientEquiv (isComplement_range_right hf) q : G) = f q :=
  by
  refine (Subtype.ext_iff.mp ?_).trans (Subtype.coe_mk (f q) ⟨q, rfl⟩)
  exact (rightQuotientEquiv (isComplement_range_right hf)).apply_eq_iff_eq_symm_apply.2 (hf q).symm

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