Theorem CategoryTheory.Limits.Concrete.initial_of_empty_of_reflects

Modification history

2024-02-01 20:02
Mathlib/CategoryTheory/Limits/Shapes/ConcreteCategory.lean
feat(CategoryTheory/Galois): evaluation is injective and more basic properties (#9841) …
Added CategoryTheory.Limits.Concrete.initial_of_empty_of_reflectsView on Github →