Commit 2025-11-28 14:12 f8c80670

View on Github →

chore(CategoryTheory): generalize EqualizerCondition.bijective_mapToEqualizer_pullback to abstract pullback cones (#31906)

Estimated changes

Modified Mathlib/CategoryTheory/Sites/Coherent/RegularSheaves.lean

added theorem CategoryTheory.regularTopology.EqualizerCondition.bijective_mapToEqualizer_pullback'

modified theorem CategoryTheory.regularTopology.EqualizerCondition.bijective_mapToEqualizer_pullback

added theorem CategoryTheory.regularTopology.EqualizerCondition.mk'

deleted def CategoryTheory.regularTopology.MapToEqualizer

added def CategoryTheory.regularTopology.mapToEqualizer

Modified Mathlib/Condensed/TopComparison.lean