comp_lift_id_right' — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

/-- If `φ : a ⟶ b` lifts `f` and `ψ : b ⟶ c` lifts `𝟙 T`, then `φ ≫ ψ` lifts `f` -/
theorem comp_lift_id_right' {R S : 𝒮} {a b c : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [p.IsHomLift f φ] (T : 𝒮) (ψ : b ⟶ c)
    [p.IsHomLift (𝟙 T) ψ] : p.IsHomLift f (φ ≫ ψ) :=
  by
  obtain rfl : S = T := by rw [← codomain_eq p f φ, domain_eq p (𝟙 T) ψ]
  infer_instance

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