English
Convexity is preserved when passing from ℝ to the restricted 𝕜-scalar structure if 𝕜 is RC-like.
Русский
Выпуклость сохраняется при переходе от ℝ к ограниченной скалярной структуре 𝕜, если 𝕜 RC-подобно.
LaTeX
$$$ \\Convex_{\\mathbb{R}}(s) \\text{ persists under restriction from } \\mathbb{R} \\text{ to } 𝕜 $$$
Lean4
/-- Construct a model with corners over `ℝ` from a continuous partial equiv with convex range. -/
def of_convex_range {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type*} [TopologicalSpace H]
(φ : PartialEquiv H E) (hsource : φ.source = univ) (htarget : Convex ℝ φ.target) (hcont : Continuous φ)
(hcont_inv : Continuous φ.symm) (hint : (interior φ.target).Nonempty) : ModelWithCorners ℝ E H
where
toPartialEquiv := φ
source_eq := hsource
convex_range' :=
by
have : range φ = φ.target := by rw [← φ.image_source_eq_target, hsource, image_univ.symm]
simp only [instIsRCLikeNormedField, ↓reduceDIte, this]
exact htarget.convex_isRCLikeNormedField
nonempty_interior' :=
by
have : range φ = φ.target := by rw [← φ.image_source_eq_target, hsource, image_univ.symm]
simp [this, hint]
