Theorems · Definition · category theory
CategoryTheory.Limits.IsFiltered.sequentialFunctor_obj
(J : Type u_2) → [Countable J] → [inst : Preorder J] → [CategoryTheory.IsFiltered 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.IsFilteredstatement and proof · cited by 210
Cited by4
Results whose statement or proof uses this declaration.
- CategoryTheory.Limits.IsFiltered.sequentialFunctorproof · cited by 2
- CategoryTheory.Limits.IsFiltered.sequentialFunctor_obj.congr_simpstatement and proof · cited by 0
- CategoryTheory.Limits.IsFiltered.sequentialFunctor_final_auxstatement and proof · cited by 0
- CategoryTheory.Limits.IsFiltered.sequentialFunctor_mapstatement and proof · cited by 0