Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-04 07:42 c939c9e4

View on Github →

feat(category_theory/limits/preserves): preserving terminal objects (#5060) Another part of #4716.

Estimated changes

Created src/category_theory/limits/preserves/shapes/terminal.lean

added theorem category_theory.limits.has_terminal_of_has_terminal_of_preserves_limit

added def category_theory.limits.is_limit_map_cone_empty_cone_equiv

added def category_theory.limits.is_limit_of_has_terminal_of_preserves_limit

added def category_theory.limits.is_terminal_obj_of_is_terminal

added def category_theory.limits.is_terminal_of_is_terminal_obj

added def category_theory.limits.preserves_terminal.iso

added theorem category_theory.limits.preserves_terminal.iso_hom

added def category_theory.limits.preserves_terminal.of_iso_comparison

added def category_theory.limits.preserves_terminal_of_is_iso

added def category_theory.limits.preserves_terminal_of_iso