Theorems · Definition · category theory
TopCat.precoverage
CategoryTheory.Precoverage TopCat
The precoverage on TopCat given by jointly surjective families of open embeddings.
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 61 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- TopCatstatement and proof · cited by 1,889
- CategoryTheory.forgetproof · cited by 418
- CategoryTheory.Precoveragestatement · cited by 204
- CategoryTheory.Precoverage.comapproof · cited by 27
- CategoryTheory.MorphismProperty.precoverageproof · cited by 23
- CategoryTheory.Types.jointlySurjectivePrecoverageproof · cited by 10
- TopCat.isOpenEmbeddingproof · cited by 2
Cited by4
Results whose statement or proof uses this declaration.
- TopCat.exists_mem_zeroHypercover_rangestatement and proof · cited by 1
- TopCat.isOpenEmbedding_f_zeroHypercoverstatement and proof · cited by 1
- TopCat.grothendieckTopologyproof · cited by 1
- TopCat.precoverage_le_comap_uliftFunctorstatement and proof · cited by 0