terminal): is_terminal object (#3957)

Commit

5 years ago

feat(category_theory/limits/shapes/terminal): is_terminal object (#3957) Add language to talk about when an object is terminal, and generalise some results to use this

References

#4925 - Make prime-avoidance branch build

Author

b-mehta

Parents

fc57cf49

mathlib3 7cd67b56 - feat(category_theory/limits/shapes/terminal): is_terminal object (#3957)

mathlib3
7cd67b56 - feat(category_theory/limits/shapes/terminal): is_terminal object (#3957)