[Merged by Bors] - doc: Clarify the use case of Function.extend#7547
[Merged by Bors] - doc: Clarify the use case of Function.extend#7547YaelDillies wants to merge 5 commits intomasterfrom
Function.extend#7547Conversation
Confusion was recently expressed so as to how to use `Function.extend`. This is an to clear it up. Also fix the name of `Injective.factorsThrough`.
bc8b9d1 to
3bbd9ec
Compare
| /-- `extend f g e'` extends a function `g : α → γ` | ||
| along a function `f : α → β` to a function `β → γ`, | ||
| by using the values of `g` on the range of `f` | ||
| and the values of an auxiliary function `e' : β → γ` elsewhere. |
There was a problem hiding this comment.
Nit: I quite liked the mnemonic of e for elsewhere
There was a problem hiding this comment.
Oh I really didn't get that mnemonic. I used j for junk.
There was a problem hiding this comment.
Sorry, I don't really see how to restore that mnemonic.
|
✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with |
Co-authored-by: Riccardo Brasca <riccardo.brasca@gmail.com>
|
bors merge |
Confusion was recently expressed so as to how to use `Function.extend`. This is an attempt to clear it up. Also fix the name of `Injective.factorsThrough`.
|
Build failed (retrying...): |
Confusion was recently expressed so as to how to use `Function.extend`. This is an attempt to clear it up. Also fix the name of `Injective.factorsThrough`.
|
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
Function.extendFunction.extend
Confusion was recently expressed so as to how to use
Function.extend. This is an attempt to clear it up.Also fix the name of
Injective.factorsThrough.