English
If s is strictly convex and f is a linear map that is continuous and injective, then the preimage f^{-1}(s) is strictly convex.
Русский
Если s строго выпукло и f — линейное отображение, непрерывное и инъективное, то прообраз f^{-1}(s) строго выпуклый.
LaTeX
$$$StrictConvex 𝕜 s \Rightarrow \forall {f : E \to F}, IsLinearMap 𝕜 f \Rightarrow Continuous f \Rightarrow Injective f \Rightarrow StrictConvex 𝕜 (Set.preimage f s)$$$
Lean4
theorem linear_preimage {s : Set F} (hs : StrictConvex 𝕜 s) (f : E →ₗ[𝕜] F) (hf : Continuous f) (hfinj : Injective f) :
StrictConvex 𝕜 (s.preimage f) := by
intro x hx y hy hxy a b ha hb hab
refine preimage_interior_subset_interior_preimage hf ?_
rw [mem_preimage, f.map_add, f.map_smul, f.map_smul]
exact hs hx hy (hfinj.ne hxy) ha hb hab
