Theorems · Definition · category theory
CategoryTheory.GrothendieckTopology.Cover.Relation.fst
{C : Type u} →
[inst : CategoryTheory.Category.{v, u} C] →
{X : C} → {J : CategoryTheory.GrothendieckTopology C} → {S : J.Cover X} → S.Relation → S.ArrowThe first arrow.
- Cited by
- 22 results in Mathlib
- Foundations
- Depth 34 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CategoryTheory.Category
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
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
- CategoryTheory.GrothendieckTopologystatement and proof · cited by 1,415
- CategoryTheory.GrothendieckTopology.Coverstatement and proof · cited by 211
- CategoryTheory.GrothendieckTopology.Cover.Arrowstatement · cited by 99
- CategoryTheory.GrothendieckTopology.Cover.Relationstatement and proof · cited by 25
Cited by26
Results whose statement or proof uses this declaration.
- CategoryTheory.GrothendieckTopology.Cover.shapeproof · cited by 147
- CategoryTheory.GrothendieckTopology.Cover.Relation.rstatement · cited by 23
- CategoryTheory.Meqproof · cited by 17
- CategoryTheory.Meq.extstatement · cited by 5
- CategoryTheory.Meq.equiv_symm_eq_applystatement · cited by 4
- CategoryTheory.Meq.conditionstatement · cited by 2
- CategoryTheory.GrothendieckTopology.Plus.eq_mk_iff_existsproof · cited by 2
- CategoryTheory.GrothendieckTopology.Plus.sepproof · cited by 2
- CategoryTheory.Meq.congr_applystatement · cited by 1
- CategoryTheory.GrothendieckTopology.Cover.index_fststatement · cited by 1
- CategoryTheory.GrothendieckTopology.Plus.inj_of_sepproof · cited by 1
- CategoryTheory.GrothendieckTopology.Plus.meqOfSepstatement · cited by 1