instHasLiftingPropertySnd — Mathlib

English

Another instance asserting liftings pass through pushout.inl under HasPushout and HasLiftingProperty.

Русский

Еще один пример того, как подъёмы проходят через pushout.inl при HasPushout и HasLiftingProperty.

LaTeX

$$$$ HasLiftingProperty(pushout.inl\\,s\\,f) p $$$$

Lean4

instance [HasPullback g t] {T₁ T₂ : C} (p : T₁ ⟶ T₂) [HasLiftingProperty p g] :
    HasLiftingProperty p (pullback.snd g t) :=
  (IsPullback.of_hasPullback g t).hasLiftingProperty p

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