of_comp_left — Mathlib

English

If i and i' both have liftings with respect to p, then the composite i ≫ i' has a lifting with respect to p.

Русский

Если i и i' имеют подъёмы по отношению к p, то композиция i ≫ i' имеет подъём по отношению к p.

LaTeX

$$$$ HasLiftingProperty\\big(i\\, p\\big) \\land HasLiftingProperty\\big(i'\\, p\\big) \\Rightarrow HasLiftingProperty\\big(i\\;\\circ\\;i', p\\big) $$$$

Lean4

instance of_comp_left [HasLiftingProperty i p] [HasLiftingProperty i' p] : HasLiftingProperty (i ≫ i') p :=
  ⟨fun {f} {g} sq => by
    have fac := sq.w
    rw [assoc] at fac
    exact
      CommSq.HasLift.mk'
        { l := (CommSq.mk (CommSq.mk fac).fac_right).lift
          fac_left := by simp only [assoc, CommSq.fac_left]
          fac_right := by simp only [CommSq.fac_right] }⟩

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