projRestricts_eq_comp — Mathlib

English

For hJK: ∀ i, J i → K i and hKL: ∀ i, K i → L i, ProjRestricts C hJK ∘ ProjRestrict C hKL = ProjRestrict C (fun i ↦ hKL i ∘ hJK i).

Русский

Для отображений hJK и hKL выполняется: ProjRestricts C hJK ∘ ProjRestrict C hKL = ProjRestrict C (i ↦ hKL i ∘ hJK i).

LaTeX

$$$$ \\mathrm{ProjRestricts}\\, C\\, h_{JK} \\circ \\mathrm{ProjRestricts}\\, C\\, h_{KL} = \\mathrm{ProjRestricts}\\, C\\, (\\lambda i. h_{KL} i \\circ h_{JK} i). $$$$

Lean4

theorem projRestricts_eq_comp (hJK : ∀ i, J i → K i) (hKL : ∀ i, K i → L i) :
    ProjRestricts C hJK ∘ ProjRestricts C hKL = ProjRestricts C (fun i ↦ hKL i ∘ hJK i) :=
  by
  ext x i
  simp only [π, Proj, Function.comp_apply, ProjRestricts_coe]
  simp_all

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