comp_lift_id_right — Mathlib

English

If φ lifts f and ψ lifts 𝟙 T, then φ ≫ ψ lifts f.

Русский

Если φ поднимает f, а ψ поднимает 𝟙 T, то φ ≫ ψ поднимает f.

LaTeX

$$$$ p.IsHomLift f (\varphi \gg \psi) $$$$

Lean4

instance comp_lift_id_right {a b c : 𝒳} {S T : 𝒮} (f : S ⟶ T) (φ : a ⟶ b) [p.IsHomLift f φ] (ψ : b ⟶ c)
    [p.IsHomLift (𝟙 T) ψ] : p.IsHomLift f (φ ≫ ψ) := by simpa using inferInstanceAs (p.IsHomLift (f ≫ 𝟙 T) (φ ≫ ψ))

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