English
The preimage of a strictly convex set under an affine map is strictly convex.
Русский
Обратное изображение строго выпуклого множества под аффинной картой является строго выпуклым.
LaTeX
$$$\StrictConvex 𝕜 s \rightarrow \forall {f : E \to^a[𝕜] F},\; Continuous (f) \rightarrow Injective (f) \rightarrow \StrictConvex 𝕜 (f^{-1}' s)$$$
Lean4
/-- The image of a strictly convex set under an affine map is strictly convex. -/
theorem affine_image (hs : StrictConvex 𝕜 s) {f : E →ᵃ[𝕜] F} (hf : IsOpenMap f) : StrictConvex 𝕜 (f '' s) :=
by
rintro _ ⟨x, hx, rfl⟩ _ ⟨y, hy, rfl⟩ hxy a b ha hb hab
exact
hf.image_interior_subset _
⟨a • x + b • y, ⟨hs hx hy (ne_of_apply_ne _ hxy) ha hb hab, Convex.combo_affine_apply hab⟩⟩
