Commit 2023-05-13 13:53 29345891

View on Github →

feat: port CategoryTheory.Subterminal (#3943)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Subterminal.lean

added theorem CategoryTheory.IsSubterminal.def

added theorem CategoryTheory.IsSubterminal.isIso_diag

added def CategoryTheory.IsSubterminal.isoDiag

added theorem CategoryTheory.IsSubterminal.mono_isTerminal_from

added theorem CategoryTheory.IsSubterminal.mono_terminal_from

added def CategoryTheory.IsSubterminal

added def CategoryTheory.Subterminals

added theorem CategoryTheory.isSubterminal_of_isIso_diag

added theorem CategoryTheory.isSubterminal_of_isTerminal

added theorem CategoryTheory.isSubterminal_of_mono_isTerminal_from

added theorem CategoryTheory.isSubterminal_of_mono_terminal_from

added theorem CategoryTheory.isSubterminal_of_terminal

added theorem CategoryTheory.monoOver_terminal_to_subterminals_comp

added def CategoryTheory.subterminalInclusion

added def CategoryTheory.subterminalsEquivMonoOverTerminal

added theorem CategoryTheory.subterminals_to_monoOver_terminal_comp_forget