Theorems · Theorem · category theory

CategoryTheory.IsPushout.hasLiftingProperty

∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y Z W : C} {f : X ⟶ Y} {s : X ⟶ Z} {g : Z ⟶ W}
  {t : Y ⟶ W},
  CategoryTheory.IsPushout s f g t →
    ∀ {Z' W' : C} (g' : Z' ⟶ W') [CategoryTheory.HasLiftingProperty f g'], CategoryTheory.HasLiftingProperty g g'

Defined in

Mathlib.CategoryTheory.LiftingProperties.Limits

Cited by

0 results in Mathlib

Foundations

Depth 30 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.HasLiftingProperty