Theorem CategoryTheory.MorphismProperty.coverage_eq_toCoverage_pretopology

Modification history

2025-09-08 18:25

Mathlib/CategoryTheory/Sites/MorphismProperty.lean

feat(CategoryTheory/Sites/MorphismProperty): add induced coverage (#28778) …

Added CategoryTheory.MorphismProperty.coverage_eq_toCoverage_pretopology View on Github →