Theorems · Theorem · category theory

CategoryTheory.Types.mem_jointlySurjectivePrecoverage_iff

∀ {X : Type u} {R : CategoryTheory.Presieve X},
  R ∈ CategoryTheory.Types.jointlySurjectivePrecoverage.coverings X ↔
    ∀ (x : X), ∃ Y g, R g ∧ x ∈ Set.range ⇑(CategoryTheory.ConcreteCategory.hom g)

Defined in: Mathlib.CategoryTheory.Sites.JointlySurjective
Cited by: 1 results in Mathlib
Foundations: Depth 14 from the axioms · uses propext, Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites9

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coestatement · cited by 62,936
Setstatement · cited by 53,352
Quiver.Homstatement · cited by 32,603
Set.rangestatement · cited by 4,705
CategoryTheory.ConcreteCategory.homstatement · cited by 4,022
TypeCat.Funstatement · cited by 1,307
CategoryTheory.Presievestatement and proof · cited by 449
CategoryTheory.Precoverage.coveringsstatement · cited by 194
CategoryTheory.Types.jointlySurjectivePrecoveragestatement · cited by 10

Cited by1

Results whose statement or proof uses this declaration.

CategoryTheory.Types.singleton_mem_jointlySurjectivePrecoverage_iffproof · cited by 0