projRestricts_eq_id — Mathlib

English

ProjRestricts C (fun i h => h) equals the identity map.

Русский

ProjRestricts C (функция, отправляющая i и h в h) равна тождественному отображению.

LaTeX

$$$$ \\mathrm{ProjRestricts}\\, C\\, (\\lambda i\\, (h:\\, J i) \\mapsto h) = \\mathrm{id}. $$$$

Lean4

theorem projRestricts_eq_id : ProjRestricts C (fun i (h : J i) ↦ h) = id :=
  by
  ext ⟨x, y, hy, rfl⟩ i
  simp +contextual only [π, Proj, ProjRestricts_coe, id_eq, if_true]

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