Wrepr_equiv — Mathlib

English

For any x in the W-type, the Wequiv relation relates Wrepr x to x.

Русский

Для любого x из W-типа Wequiv связывает Wrepr x с x.

LaTeX

$$$$\forall {F : Type u \to Type v} [q : QPF F] (x : (q.P F).W), Wequiv (Wrepr x) x.$$$$

Lean4

theorem Wrepr_equiv (x : q.P.W) : Wequiv (Wrepr x) x :=
  by
  induction x with
  | _ a f ih
  apply Wequiv.trans
  · change Wequiv (Wrepr ⟨a, f⟩) (PFunctor.W.mk (q.P.map Wrepr ⟨a, f⟩))
    apply Wequiv.abs'
    have : Wrepr ⟨a, f⟩ = PFunctor.W.mk (repr (abs (q.P.map Wrepr ⟨a, f⟩))) := rfl
    rw [this, PFunctor.W.dest_mk, abs_repr]
    rfl
  apply Wequiv.ind; exact ih

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