Theorems · Theorem · category theory

CategoryTheory.AB5OfSize_of_univLE

∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasFilteredColimitsOfSize.{w₂, w₂', v, u} C] [inst_2 : UnivLE.{w, w₂}]
  [inst_3 : UnivLE.{w', w₂'}] [CategoryTheory.AB5OfSize.{w₂, w₂', v, u} C], CategoryTheory.AB5OfSize.{w, w', v, u} C

Defined in

Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasFilteredColimitsOfSizeUnivLEUnivLECategoryTheory.AB5OfSize