proj_pi — Mathlib

English

Projection onto coordinate i is inverse to pi, i.e., projecting after pi recovers the i-th component.

Русский

Проекция на i-ю координату обратно восстанавливает i-й компонент после применения pi.

LaTeX

$$$\text{proj}_i(\mathrm{Path.Homotopic.pi}\; paths) = paths_i$$$

Lean4

/-- Lemmas showing projection is the inverse of pi. -/
@[simp]
theorem proj_pi (i : ι) (paths : ∀ i, Path.Homotopic.Quotient (as i) (bs i)) : proj i (pi paths) = paths i :=
  by
  induction paths using Quotient.induction_on_pi
  rw [proj, pi_lift, ← Path.Homotopic.map_lift]
  congr

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