comp_lift_id_left — Mathlib

English

If a = b in X and p.obj a = R, then p.IsHomLift (eqToHom h) (eqToHom hab) where hab: a = b.

Русский

Пусть a = b в X и p.obj a = R. Тогда p.IsHomLift (eqToHom h) (eqToHom hab) при hab: a = b.

LaTeX

$$$$ p.IsHomLift (eqToHom h) (eqToHom hab) $$$$

Lean4

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

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