Theorems · Definition · category theory
CategoryTheory.Limits.IsCofiltered.sequentialFunctor_obj
(J : Type u_2) → [Countable J] → [inst : Preorder J] → [CategoryTheory.IsCofiltered J] → ℕ → J
The object part of the initial functor ℕᵒᵖ ⥤ J
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 18 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Preorderstatement and proof · cited by 7,952
- Countablestatement and proof · cited by 633
- CategoryTheory.IsCofilteredstatement and proof · cited by 133
Cited by4
Results whose statement or proof uses this declaration.
- CategoryTheory.Limits.IsCofiltered.sequentialFunctorproof · cited by 2
- CategoryTheory.Limits.IsCofiltered.sequentialFunctor_initial_auxstatement and proof · cited by 0
- CategoryTheory.Limits.IsCofiltered.sequentialFunctor_mapstatement and proof · cited by 0
- CategoryTheory.Limits.IsCofiltered.sequentialFunctor_obj.congr_simpstatement and proof · cited by 0