Commit 2021-07-23 10:09 f2f62286
View on Github →feat(set/basic): range_splitting f : range f → α (#8340)
We use choice to provide an arbitrary injective splitting range f → α for any f : α → β.
feat(set/basic): range_splitting f : range f → α (#8340)
We use choice to provide an arbitrary injective splitting range f → α for any f : α → β.