mathlib
f2f62286 - feat(set/basic): range_splitting f : range f → α (#8340)

Commit

4 years ago

feat(set/basic): range_splitting f : range f → α (#8340) We use choice to provide an arbitrary injective splitting `range f → α` for any `f : α → β`.

Author

kim-em

Parents