Mathlib Changelog
v4
Changelog
About
Github
Theorem
CategoryTheory.initiallySmall_of_essentiallySmall_weakly_initial_objectProperty
Modification history
2026-06-18 11:17
Mathlib/CategoryTheory/Limits/FinallySmall.lean
feat(AlgebraicGeometry): points of the small étale site (#35136) …
Added
CategoryTheory.initiallySmall_of_essentiallySmall_weakly_initial_objectProperty
View on Github →