proj_comp_transitionMapLE — Mathlib

English

For S and n ≤ m the projection to m followed by the diagram’s map equals the projection to n; i.e., proj m ≫ diagram.map ⟨homOfLE h⟩ = proj n.

Русский

Для S и n ≤ m композиция proj m с диаграммной картой равна proj n.

LaTeX

$$$S.proj(m) \; \; \; \; \; \; \; \; \; \; \\; S.diagram.map(\langle homOfLE(h)\rangle) = S.proj(n)$$$

Lean4

theorem proj_comp_transitionMapLE {n m : ℕ} (h : n ≤ m) : S.proj m ≫ S.diagram.map ⟨homOfLE h⟩ = S.proj n :=
  S.asLimitCone.w (homOfLE h).op

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