Commit 2025-01-19 08:58 9b6fa8d7

feat: in one dimension, a point is either isolated or a point of unique differentiability (#20827) A point in a subset of a field is either a point of unique differentials, or isolated. In both cases, there is a definite value for the derivative of a map (its unique derivative in the former case, zero in the latter case). This means there is no choice involved, contrary to what happens in higher dimension. This remark means we can remove many UniqueDiffWithinAt assumptions in one-dimensional settings. This PR proves the new lemma that a point is either isolated or a point of unique differentiability. The application to cleanup the library will be in a further PR (#20816)