Theorem small_of_injective_of_exists

Modification history

2023-09-08 11:01
Mathlib/Logic/Small/Basic.lean
feat: a functor from a small category to a filtered category factors through a small filtered category (#6212)
Added small_of_injective_of_existsView on Github →