quotientEquivOfIsCompl_symm_apply

English

Symmetry facts: the quotient equivalence (p.quotientEquivOfIsCompl q h).symm behaves predictably on mk and mk.coe; in particular, applying symm to a quotient element yields the representative in E completing the diagram.

Русский

Симметрические факты: отображение p.quotientEquivOfIsCompl q h и его симметрическое применение к элементу косвенно возвращают представителя в E, согласуя диаграмму.

LaTeX

$$$(p.quotientEquivOfIsCompl q h).symm$ acts as expected on mk and coe$$

Lean4

@[simp]
theorem quotientEquivOfIsCompl_symm_apply (h : IsCompl p q) (x : q) :
    -- Porting note: type ascriptions needed on the RHS
    (quotientEquivOfIsCompl p q h).symm x = (Quotient.mk x : E ⧸ p) :=
  rfl

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