wrepr_equiv — Mathlib

English

The canonical representative map lands in the same quotient class, i.e., WEquiv (wrepr x) x.

Русский

Каноническое представление отображает элемент в ту же эквивалентную по отношению к кват/квату клаccу.

LaTeX

$$$\forall {\alpha : TypeVec n} (x : q.P.W \alpha), WEquiv (wrepr x) x$$$

Lean4

theorem wrepr_equiv {α : TypeVec n} (x : q.P.W α) : WEquiv (wrepr x) x :=
  by
  apply q.P.w_ind _ x; intro a f' f ih
  apply WEquiv.trans _ (q.P.wMk' (appendFun id wrepr <$$> ⟨a, q.P.appendContents f' f⟩))
  · apply wEquiv.abs'
    rw [wrepr_wMk, q.P.wDest'_wMk', q.P.wDest'_wMk', abs_repr]
  rw [q.P.map_eq, MvPFunctor.wMk', appendFun_comp_splitFun, id_comp]
  apply WEquiv.ind; exact ih

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