Theorems · Definition · category theory

CategoryTheory.MorphismProperty.IsStableUnderCobaseChangeAlong.recOn

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {P : CategoryTheory.MorphismProperty C} →
      {X Y : C} →
        {f : X ⟶ Y} →
          {motive : P.IsStableUnderCobaseChangeAlong f → Sort u_1} →
            (t : P.IsStableUnderCobaseChangeAlong f) →
              ((of_isPushout :
                    ∀ {Z W : C} {f' : Z ⟶ W} {g' : Y ⟶ W} {g : X ⟶ Z},
                      CategoryTheory.IsPushout f g g' f' → P g → P g') →
                  motive ⋯) →
                motive t

Defined in

Mathlib.CategoryTheory.MorphismProperty.Limits

Cited by

0 results in Mathlib

Foundations

Depth 6 from the axioms · uses no axioms

Assumes

CategoryTheory.Category