instHasLiftingPropertyInr — Mathlib

English

If s ⟶ f is a pushout, HasLiftingProperty s p implies HasLiftingProperty (pushout.inr s f) p.

Русский

Если s ⟶ f образует pushout и HasLiftingProperty s p, то HasLiftingProperty (pushout.inr s f) p.

LaTeX

$$$$ HasLiftingProperty\\big(pushout.inr\\,s\\,f\\,, p\\big) $$$$

Lean4

instance [HasPushout s f] {T₁ T₂ : C} (p : T₁ ⟶ T₂) [HasLiftingProperty s p] : HasLiftingProperty (pushout.inr s f) p :=
  (IsPushout.of_hasPushout s f).flip.hasLiftingProperty p

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