mathlib
aa78feba - feat(category_theory/is_connected): constant functor is full (#8233)

Commit

4 years ago

feat(category_theory/is_connected): constant functor is full (#8233) Shows the constant functor on a connected category is full. Also golfs a later proof slightly.

References

random_variable2

Author

b-mehta

Parents

b1806d19

mathlib aa78feba - feat(category_theory/is_connected): constant functor is full (#8233)

mathlib
aa78feba - feat(category_theory/is_connected): constant functor is full (#8233)