Stream: math-comp analysis

Topic: "glue" in functions.v

view this post on Zulip Julien Puydt (Dec 05 2022 at 17:44):

Why does it require the ranges to be disjoint? As far as I know the most common use of glueing is to define functions by cases, and the glued parts all have the very same target...

view this post on Zulip Cyril Cohen (Dec 05 2022 at 18:17):

Last updated: Jan 30 2023 at 12:03 UTC