Commit 2023-03-07 15:31 11a27e2c

View on Github →

feat: port CategoryTheory.Limits.Shapes.StrictInitial (#2695)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Limits/Shapes/StrictInitial.lean

added theorem CategoryTheory.Limits.IsInitial.isIso_to

added theorem CategoryTheory.Limits.IsInitial.strict_hom_ext

added theorem CategoryTheory.Limits.IsInitial.subsingleton_to

added theorem CategoryTheory.Limits.IsTerminal.isIso_from

added theorem CategoryTheory.Limits.IsTerminal.strict_hom_ext

added theorem CategoryTheory.Limits.IsTerminal.subsingleton_to

added theorem CategoryTheory.Limits.hasStrictInitialObjects_of_initial_is_strict

added theorem CategoryTheory.Limits.hasStrictTerminalObjects_of_terminal_is_strict

added theorem CategoryTheory.Limits.initial.hom_ext

added theorem CategoryTheory.Limits.initial.subsingleton_to

added theorem CategoryTheory.Limits.initialMul_inv

added theorem CategoryTheory.Limits.isInitialMul_inv

added theorem CategoryTheory.Limits.limit_π_isIso_of_is_strict_terminal

added theorem CategoryTheory.Limits.mulInitial_inv

added theorem CategoryTheory.Limits.mulIsInitial_inv

added theorem CategoryTheory.Limits.terminal.hom_ext

added theorem CategoryTheory.Limits.terminal.subsingleton_to