Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-07 15:41 dcbb59c4

View on Github →

feat(category_theory/limits): is_limit.exists_unique (#11875) Yet another restatement of the limit property which is occasionally useful.

Estimated changes

Modified src/category_theory/limits/has_limits.lean

added theorem category_theory.limits.colimit.exists_unique

added theorem category_theory.limits.limit.exists_unique

Modified src/category_theory/limits/is_limit.lean

added theorem category_theory.limits.is_colimit.exists_unique

added def category_theory.limits.is_colimit.of_exists_unique

added theorem category_theory.limits.is_limit.exists_unique

added def category_theory.limits.is_limit.of_exists_unique

Modified src/category_theory/limits/shapes/equalizers.lean

added theorem category_theory.limits.coequalizer.exists_unique

added theorem category_theory.limits.cofork.is_colimit.exists_unique

added def category_theory.limits.cofork.is_colimit.of_exists_unique

added theorem category_theory.limits.equalizer.exists_unique

added theorem category_theory.limits.fork.is_limit.exists_unique

added def category_theory.limits.fork.is_limit.of_exists_unique