Theorems · Definition · category theory
CategoryTheory.CardinalFilteredPoset.cocone
Deprecated since 2026-06-24Use CategoryTheory.CardinalDirectedPoset.cocone instead.
{κ : Cardinal.{u}} →
[inst : Fact κ.IsRegular] →
(J : CategoryTheory.CardinalDirectedPoset κ) →
CategoryTheory.Limits.Cocone (CategoryTheory.CardinalDirectedPoset.functorOfPredicateSet J.PropSet)Alias of CategoryTheory.CardinalDirectedPoset.cocone.
For any object J : CardinalDirectedPoset κ, this is a colimit
cocone exhibiting J as the colimit of its subsets
that are of cardinality < κ and have a terminal object.
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 73 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Fact
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites13
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement · cited by 53,352
- Factstatement · cited by 2,726
- Cardinalstatement · cited by 2,598
- CategoryTheory.ObjectProperty.FullSubcategory.objstatement · cited by 1,316
- CategoryTheory.Limits.Coconestatement · cited by 746
- Cardinal.IsRegularstatement · cited by 282
- PartOrdEmbstatement · cited by 68
- PartOrdEmb.carrierstatement · cited by 61
- PartOrdEmb.isCardinalFilteredstatement · cited by 25
- CategoryTheory.CardinalDirectedPosetstatement · cited by 24
- CategoryTheory.CardinalDirectedPoset.functorOfPredicateSetstatement · cited by 6
- CategoryTheory.CardinalDirectedPoset.PropSetstatement · cited by 3
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.