Theorems · Definition · category theory
CategoryTheory.CardinalDirectedPoset
(κ : Cardinal.{u}) → [Fact κ.IsRegular] → Type (u + 1)The category of κ-filtered partially ordered types,
with morphisms given by order embeddings.
- Cited by
- 24 results in Mathlib
- Foundations
- Depth 22 from the axioms · uses propext, Quot.sound
- Assumes
- Fact
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Factstatement and proof · cited by 2,726
- Cardinalstatement and proof · cited by 2,598
- CategoryTheory.ObjectProperty.FullSubcategoryproof · cited by 726
- Cardinal.IsRegularstatement and proof · cited by 282
- PartOrdEmb.isCardinalFilteredproof · cited by 25
Cited by54
Results whose statement or proof uses this declaration.
- CategoryTheory.CardinalDirectedPoset.functorOfPredicateSetstatement and proof · cited by 6
- CategoryTheory.CardinalDirectedPoset.PropSetWithTopstatement and proof · cited by 5
- CategoryTheory.CardinalDirectedPoset.withTopstatement and proof · cited by 5
- CategoryTheory.CardinalDirectedPoset.PropSetstatement and proof · cited by 3
- CategoryTheory.CardinalDirectedPoset.isCardinalPresentable_iffstatement and proof · cited by 3
- CategoryTheory.CardinalDirectedPoset.coconeOfPredicateSetstatement and proof · cited by 2
- CategoryTheory.CardinalDirectedPoset.Hom.injectivestatement and proof · cited by 2
- CategoryTheory.CardinalDirectedPoset.Hom.le_iff_lestatement and proof · cited by 2
- CategoryTheory.CardinalDirectedPoset.isCardinalPresentable_iff'statement and proof · cited by 2
- CategoryTheory.CardinalDirectedPoset.isCardinalPresentable_of_hasCardinalLT_of_lestatement and proof · cited by 2
- CategoryTheory.CardinalDirectedPoset.propSetWithTop_pairstatement and proof · cited by 2
- CategoryTheory.CardinalDirectedPoset.coconeWithTopstatement and proof · cited by 1