Theorems · Definition · category theory
PartOrdEmb.isCardinalFiltered
(κ : Cardinal.{u}) → [Fact κ.IsRegular] → CategoryTheory.ObjectProperty PartOrdEmbThe property of objects in PartOrdEmb that are
satisfied by κ-directed partially ordered types.
(Note: for partially ordered types, "κ-directed" and
"κ-filtered" are synonyms. This is implemented using the
categorical notion IsCardinalFiltered.)
- Cited by
- 25 results in Mathlib
- Foundations
- Depth 21 from the axioms · uses propext, Quot.sound
- Assumes
- Fact
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
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.ObjectPropertystatement · cited by 798
- Cardinal.IsRegularstatement and proof · cited by 282
- CategoryTheory.IsCardinalFilteredproof · cited by 69
- PartOrdEmbstatement and proof · cited by 68
- PartOrdEmb.carrierproof · cited by 61
Cited by50
Results whose statement or proof uses this declaration.
- CategoryTheory.CardinalDirectedPosetproof · cited by 24
- CategoryTheory.CardinalDirectedPoset.functorOfPredicateSetstatement and proof · cited by 6
- CategoryTheory.CardinalDirectedPoset.PropSetWithTopstatement · cited by 5
- CategoryTheory.CardinalDirectedPoset.isCardinalPresentable_iffstatement and proof · cited by 3
- CategoryTheory.CardinalDirectedPoset.PropSetstatement · cited by 3
- CategoryTheory.CardinalDirectedPoset.Hom.injectivestatement · cited by 2
- CategoryTheory.CardinalDirectedPoset.Hom.le_iff_lestatement · cited by 2
- CategoryTheory.CardinalDirectedPoset.isCardinalPresentable_iff'statement · cited by 2
- CategoryTheory.CardinalDirectedPoset.isCardinalPresentable_of_hasCardinalLT_of_lestatement and proof · cited by 2
- CategoryTheory.CardinalDirectedPoset.propSetWithTop_pairstatement · cited by 2
- CategoryTheory.CardinalDirectedPoset.coconeOfPredicateSetstatement · cited by 2
- CategoryTheory.CardinalDirectedPoset.hasCardinalLTWithTerminalstatement · cited by 1