projRestricts_comp_projRestrict — Mathlib

English

For h: ∀ i, J i → K i, ProjRestricts C h ∘ ProjRestrict C K = ProjRestrict C J.

Русский

Для h: ∀ i, J i → K i, выполняется ProjRestricts C h ∘ ProjRestrict C K = ProjRestrict C J.

LaTeX

$$$$ \\mathrm{ProjRestricts}\\, C\\, h \\circ \\mathrm{ProjRestrict}\\, C\\, K = \\mathrm{ProjRestrict}\\, C\\, J.$$$$

Lean4

theorem projRestricts_comp_projRestrict (h : ∀ i, J i → K i) :
    ProjRestricts C h ∘ ProjRestrict C K = ProjRestrict C J :=
  by
  ext x i
  simp only [π, Proj, Function.comp_apply, ProjRestricts_coe, ProjRestrict_coe]
  simp_all

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