Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-15 08:35 395eb2ba

View on Github →

feat(category_theory): subterminal objects (#5669)

Estimated changes

Created src/category_theory/subterminal.lean

added theorem category_theory.is_subterminal.def

added def category_theory.is_subterminal.is_iso_diag

added def category_theory.is_subterminal.iso_diag

added theorem category_theory.is_subterminal.mono_is_terminal_from

added theorem category_theory.is_subterminal.mono_terminal_from

added def category_theory.is_subterminal

added theorem category_theory.is_subterminal_of_is_iso_diag

added theorem category_theory.is_subterminal_of_is_terminal

added theorem category_theory.is_subterminal_of_mono_is_terminal_from

added theorem category_theory.is_subterminal_of_mono_terminal_from

added theorem category_theory.is_subterminal_of_terminal

added def category_theory.subterminal_inclusion

added def category_theory.subterminals