of_comp_right — Mathlib

English

If HasLiftingProperty i p and HasLiftingProperty i p', then HasLiftingProperty i (p ≫ p').

Русский

Если HasLiftingProperty(i,p) и HasLiftingProperty(i,p'), то HasLiftingProperty(i,(p∘p')).

LaTeX

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

Lean4

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

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