Theorems · Theorem · category theory
CategoryTheory.isFiltered_of_isCardinalFiltered
∀ (J : Type u) [inst : CategoryTheory.Category.{v, u} J] (κ : Cardinal.{w}) [hκ : Fact κ.IsRegular]
[CategoryTheory.IsCardinalFiltered J κ], CategoryTheory.IsFiltered J- Cited by
- 18 results in Mathlib
- Foundations
- Depth 91 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites16
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Categorystatement and proof · cited by 32,673
- CategoryTheory.Functorproof · cited by 16,252
- Factstatement and proof · cited by 2,726
- Cardinalstatement and proof · cited by 2,598
- CategoryTheory.Arrowproof · cited by 713
- CategoryTheory.SmallCategoryproof · cited by 480
- Fact.outproof · cited by 328
- Cardinal.IsRegularstatement and proof · cited by 282
- CategoryTheory.IsFilteredstatement · cited by 210
- CategoryTheory.FinCategoryproof · cited by 107
- HasCardinalLTproof · cited by 99
- CategoryTheory.IsCardinalFilteredstatement and proof · cited by 69
Cited by19
Results whose statement or proof uses this declaration.
- CategoryTheory.IsCardinalPresentable.exists_eq_of_isColimit'proof · cited by 2
- HasCardinalLT.isCardinalPresentableproof · cited by 1
- CategoryTheory.IsCardinalFiltered.exists_cardinal_directedproof · cited by 1
- CategoryTheory.IsGrothendieckAbelian.IsPresentable.injectivity₀proof · cited by 1
- CategoryTheory.IsGrothendieckAbelian.IsPresentable.surjectivityproof · cited by 1
- CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.final_functorproof · cited by 1
- CategoryTheory.isCardinalFiltered_aleph0_iffproof · cited by 1
- CategoryTheory.IsCardinalPresentable.exists_eq_of_isColimitproof · cited by 1
- CategoryTheory.Functor.Accessible.Limits.isColimitMapCoconeproof · cited by 1
- CategoryTheory.IsCardinalFiltered.multicoequalizerproof · cited by 0