(Pre)images of strict convex sets under continuous linear equivalences

In this file we prove that the (pre)image of a strict convex set under a continuous linear equivalence is a strict convex set.

@[simp]

theorem ContinuousLinearEquiv.strictConvex_preimage {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [Field 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] {s : Set F} (e : E ≃L[𝕜] F) : StrictConvex 𝕜 (⇑e ⁻¹' s) ↔ StrictConvex 𝕜 s

@[simp]

theorem ContinuousLinearEquiv.strictConvex_image {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [Field 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] {s : Set E} (e : E ≃L[𝕜] F) : StrictConvex 𝕜 (⇑e '' s) ↔ StrictConvex 𝕜 s