Theorem CategoryTheory.MorphismProperty.pretopology_monotone

Modification history

2025-09-08 18:25

Mathlib/CategoryTheory/Sites/MorphismProperty.lean

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

Added CategoryTheory.MorphismProperty.pretopology_monotone View on Github →