Theorem CategoryTheory.MorphismProperty.locallyCoverDense_forget_of_le

Modification history

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