Theorem CategoryTheory.extensive_regular_generate_coherent

Modification history

2024-02-10 10:41
Mathlib/CategoryTheory/Sites/Coherent/Comparison.lean
chore(CategoryTheory/Sites): reorganise the material related to the coherent, regular and extensive topologies (#9944) …
Modified CategoryTheory.extensive_regular_generate_coherentView on Github →
2023-11-30 10:58
Mathlib/CategoryTheory/Sites/RegularExtensive.lean
feat(CategoryTheory): `Preregular` and `FinitaryPreExtensive` implies `Precoherent` (#8643) …
Modified CategoryTheory.extensive_regular_generate_coherentView on Github →
2023-10-28 11:22
Mathlib/CategoryTheory/Sites/RegularExtensive.lean
feat: Remove `Extensive` in favour of `FinitaryExtensive`. (#7731)
Modified CategoryTheory.extensive_regular_generate_coherentView on Github →
2023-10-03 12:58
Mathlib/CategoryTheory/Sites/RegularExtensive.lean
feat: the union of the regular and extensive coverages generates the coherent topology (#6876) …
Added CategoryTheory.extensive_regular_generate_coherentView on Github →