Commit 2023-05-15 10:07 9bf37f69

View on Github →

feat: port CategoryTheory.Sites.InducedTopology (#3995)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Sites/InducedTopology.lean

added theorem CategoryTheory.CoverDense.locallyCoverDense

added def CategoryTheory.LocallyCoverDense.inducedTopology

added theorem CategoryTheory.LocallyCoverDense.inducedTopology_coverLifting

added theorem CategoryTheory.LocallyCoverDense.inducedTopology_coverPreserving

added theorem CategoryTheory.LocallyCoverDense.pushforward_cover_iff_cover_pullback

added def CategoryTheory.LocallyCoverDense

added theorem CategoryTheory.over_forget_locallyCoverDense