English
For any ModelWithCorners I, the real-convex hull of the range of I.toFun' is convex; in particular, the range itself is convex in the real sense.
Русский
Для любой модели с углами I выпуклая оболочка диапазона I.toFun' выпукла; следовательно, сам диапазон выпукл по отношению к реалям.
LaTeX
$$$ \\Convex_{\\mathbb{R}}(\\mathrm{range}(I.toFun')) $$$
Lean4
theorem convex_range [NormedSpace ℝ E] : Convex ℝ (range I) :=
by
by_cases h : IsRCLikeNormedField 𝕜
· letI : RCLike 𝕜 := h.rclike
have W := I.convex_range'
simp only [h, ↓reduceDIte, toPartialEquiv_coe] at W
simp only [Convex, StarConvex] at W ⊢
intro u hu v hv a b ha hb hab
convert W hu hv ha hb hab using 2
· rw [← @algebraMap_smul (R := ℝ) (A := 𝕜)]
rfl
· rw [← @algebraMap_smul (R := ℝ) (A := 𝕜)]
rfl
· simp [range_eq_univ_of_not_isRCLikeNormedField I h, convex_univ]
