comp_of_lift_id — Mathlib

English

If φ lifts 𝟙 R and ψ lifts 𝟙 R, then φ ≫ ψ lifts 𝟙 R.

Русский

Если φ и ψ поднимают идентичность 𝟙 R, то их композиция также поднимает 𝟙 R.

LaTeX

$$$$ p.IsHomLift (\mathsf{Id}_R) (\varphi \gg \psi) $$$$

Lean4

/-- If `φ : a ⟶ b` and `ψ : b ⟶ c` lift `𝟙 R`, then so does `φ ≫ ψ` -/
instance comp_of_lift_id (R : 𝒮) {a b c : 𝒳} (φ : a ⟶ b) (ψ : b ⟶ c) [p.IsHomLift (𝟙 R) φ] [p.IsHomLift (𝟙 R) ψ] :
    p.IsHomLift (𝟙 R) (φ ≫ ψ) :=
  comp_id (𝟙 R) ▸ comp p (𝟙 R) (𝟙 R) φ ψ

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