English
If 𝕜 is RC-like and E is a real normed space, then the range of I.toFun' is convex over ℝ.
Русский
Если 𝕜 RC-подобно, а E — реал пространства нормы, то диапазон I.toFun' выпукл по ℝ.
LaTeX
$$$ \\Convex_{\\mathbb{R}}(\\mathrm{range}(I.toFun')) $$$
Lean4
/-- If a set is `ℝ`-convex for some normed space structure, then it is `ℝ`-convex for the
normed space structure coming from an `IsRCLikeNormedField 𝕜`. Useful when constructing model
spaces to avoid diamond issues when populating the field `convex_range'`. -/
theorem _root_.Convex.convex_isRCLikeNormedField [NormedSpace ℝ E] [h : IsRCLikeNormedField 𝕜] {s : Set E}
(hs : Convex ℝ s) :
letI := h.rclike
letI := NormedSpace.restrictScalars ℝ 𝕜 E
Convex ℝ s :=
by
letI := h.rclike
letI := NormedSpace.restrictScalars ℝ 𝕜 E
simp only [Convex, StarConvex] at hs ⊢
intro u hu v hv a b ha hb hab
convert hs hu hv ha hb hab using 2
· rw [← @algebraMap_smul (R := ℝ) (A := 𝕜), ← @algebraMap_smul (R := ℝ) (A := 𝕜)]
· rw [← @algebraMap_smul (R := ℝ) (A := 𝕜), ← @algebraMap_smul (R := ℝ) (A := 𝕜)]
