English
If s is strictly convex, the image under an open linear map is strictly convex.
Русский
Если s строго выпукло, образ линейного отображения с открытым образом также строго выпукл.
LaTeX
$$$StrictConvex 𝕜 s \Rightarrow \forall f:\
E \to F, IsOpenMap f \Rightarrow StrictConvex 𝕜 (Set.image f s)$$$
Lean4
theorem linear_image [Semiring 𝕝] [Module 𝕝 E] [Module 𝕝 F] [LinearMap.CompatibleSMul E F 𝕜 𝕝] (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
refine hf.image_interior_subset _ ⟨a • x + b • y, hs hx hy (ne_of_apply_ne _ hxy) ha hb hab, ?_⟩
rw [map_add, f.map_smul_of_tower a, f.map_smul_of_tower b]
