English
The range of I has the property UniqueDiffOn with respect to 𝕜; in particular, in the RC-like case it follows from convexity and nonempty interior; otherwise the range is all of E and trivially satisfies UniqueDiffOn.
Русский
Диапазон I обладает свойством UniqueDiffOn относительно 𝕜; в частности, в RC-подобном случае следует из выпуклости и ненулевого Interior; иначе диапазон равен всему E и удовлетворяет UniqueDiffOn.
LaTeX
$$$ \\text{UniqueDiffOn } \\mathbb{K} (\\mathrm{range}(I.toFun')) $$$
Lean4
protected theorem uniqueDiffOn : UniqueDiffOn 𝕜 (range I) :=
by
by_cases h : IsRCLikeNormedField 𝕜
· letI := h.rclike 𝕜
letI := NormedSpace.restrictScalars ℝ 𝕜 E
apply uniqueDiffOn_convex_of_isRCLikeNormedField _ I.nonempty_interior
simpa [h] using I.convex_range
· simp [range_eq_univ_of_not_isRCLikeNormedField I h, uniqueDiffOn_univ]
