Theorems · Definition · category theory
CategoryTheory.IsCofiltered.minToRight
{C : Type u} →
[inst : CategoryTheory.Category.{v, u} C] →
[inst_1 : CategoryTheory.IsCofilteredOrEmpty C] → (j j' : C) → CategoryTheory.IsCofiltered.min j j' ⟶ j'minToRight j j' is an arbitrary choice of morphism from min j j' to j',
whose existence is ensured by IsCofiltered.
- Defined in
- Mathlib.CategoryTheory.Filtered.Basic
- Cited by
- 7 results in Mathlib
- Foundations
- Depth 11 from the axioms · uses Classical.choice
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Categorystatement and proof · cited by 32,673
- Quiver.Homstatement · cited by 32,603
- CategoryTheory.IsCofilteredOrEmptystatement and proof · cited by 55
- CategoryTheory.IsCofiltered.minstatement · cited by 8
Cited by8
Results whose statement or proof uses this declaration.
- CategoryTheory.IsCofiltered.inf_objs_existsproof · cited by 7
- CategoryTheory.Functor.IsEventuallyConstantTo.coneπAppproof · cited by 4
- CategoryTheory.IsCofilteredOrEmpty.of_left_adjointproof · cited by 3
- CategoryTheory.Comma.isCofiltered_of_isCofiltered_costructuredArrowproof · cited by 3
- CategoryTheory.IsCofilteredOrEmpty.isPreconnectedproof · cited by 1
- CategoryTheory.Functor.IsEventuallyConstantTo.coneπApp_eqproof · cited by 1
- CategoryTheory.Comma.initial_fst_of_isCofiltered_costructuredArrowproof · cited by 1