Theorems · Theorem · category theory
CategoryTheory.finallySmall_of_small_weakly_terminal_set
∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] [CategoryTheory.IsFilteredOrEmpty J] (s : Set J)
[Small.{v, u} ↑s], (∀ (i : J), ∃ j ∈ s, Nonempty (i ⟶ j)) → CategoryTheory.FinallySmall J- Cited by
- 2 results in Mathlib
- Foundations
- Depth 51 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
- CategoryTheory.Categorystatement and proof · cited by 32,673
- Quiver.Homstatement and proof · cited by 32,603
- Set.Elemstatement and proof · cited by 7,166
- Smallstatement and proof · cited by 369
- CategoryTheory.Functor.Finalproof · cited by 112
- CategoryTheory.ObjectProperty.ιproof · cited by 95
- CategoryTheory.IsFilteredOrEmptystatement and proof · cited by 55
- CategoryTheory.FinallySmallstatement · cited by 16
- CategoryTheory.Functor.final_of_exists_of_isFiltered_of_fullyFaithfulproof · cited by 3
- CategoryTheory.finallySmall_of_final_of_essentiallySmallproof · cited by 1
Cited by2
Results whose statement or proof uses this declaration.
- CategoryTheory.Limits.isIndObject_colimitproof · cited by 2
- CategoryTheory.finallySmall_iff_exists_small_weakly_terminal_setproof · cited by 0