Theorem CategoryTheory.coherentTopology.isLocallySurjective_π_app_zero_of_isLocallySurjective_map

Modification history

2025-07-04 07:44
Mathlib/CategoryTheory/Sites/Coherent/SequentialLimit.lean
chore: further whitespace fixes (#26708) …
Modified CategoryTheory.coherentTopology.isLocallySurjective_π_app_zero_of_isLocallySurjective_mapView on Github →
2024-11-15 12:23
Mathlib/CategoryTheory/Sites/Coherent/SequentialLimit.lean
feat(Condensed): a sequential limit of epimorphisms in light condensed modules is epimorphic (#18336) …
Added CategoryTheory.coherentTopology.isLocallySurjective_π_app_zero_of_isLocallySurjective_mapView on Github →