pi_proj — Mathlib

English

The projection pi and the lift maps are inverses when applied to a compatible family of path-homotopy classes.

Русский

Пусть имеется совместимая семейство классов гомотопий путей; проекция и лефт-проекция образуют обратное отображение.

LaTeX

$$$\mathrm{pi\;proj} : \mathrm{Path.Homotopic.pi}(paths) \mapsto paths$$$

Lean4

@[simp]
theorem pi_proj (p : Path.Homotopic.Quotient as bs) : (pi fun i => proj i p) = p :=
  by
  induction p using Quotient.inductionOn
  simp_rw [proj, ← Path.Homotopic.map_lift]
  erw [pi_lift]
  congr

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