Theorem CategoryTheory.Precoverage.locallyCoverDense_of_map_functorPullback_mem

Modification history

2026-03-04 16:50
Mathlib/CategoryTheory/Sites/DenseSubsite/InducedTopology.lean
feat(CategoryTheory/MorphismProperty): API for sites on `P.Over ⊤ X` (#36126) …
Added CategoryTheory.Precoverage.locallyCoverDense_of_map_functorPullback_memView on Github →