(Strict) convexity and linear isometries

In this file we prove some basic lemmas about (strict) convexity and linear isometries.

@[simp]

theorem LinearIsometryEquiv.strictConvex_preimage {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedField 𝕜] [PartialOrder 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set F} (e : E ≃ₗᵢ[𝕜] F) : StrictConvex 𝕜 (⇑e ⁻¹' s) ↔ StrictConvex 𝕜 s

@[simp]

theorem LinearIsometryEquiv.strictConvex_image {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedField 𝕜] [PartialOrder 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} (e : E ≃ₗᵢ[𝕜] F) : StrictConvex 𝕜 (⇑e '' s) ↔ StrictConvex 𝕜 s

theorem StrictConvex.linearIsometry_preimage {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedField 𝕜] [PartialOrder 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set F} (hs : StrictConvex 𝕜 s) (e : E →ₗᵢ[𝕜] F) : StrictConvex 𝕜 (⇑e ⁻¹' s)

theorem LinearIsometryEquiv.strictConvexSpace_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedField 𝕜] [PartialOrder 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (e : E ≃ₗᵢ[𝕜] F) : StrictConvexSpace 𝕜 E ↔ StrictConvexSpace 𝕜 F

theorem LinearIsometry.strictConvexSpace_range_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedField 𝕜] [PartialOrder 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (e : E →ₗᵢ[𝕜] F) : StrictConvexSpace 𝕜 ↥(↑e).range ↔ StrictConvexSpace 𝕜 E

instance LinearIsometry.strictConvexSpace_range {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedField 𝕜] [PartialOrder 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [StrictConvexSpace 𝕜 E] (e : E →ₗᵢ[𝕜] F) : StrictConvexSpace 𝕜 ↥(↑e).range

theorem LinearIsometry.strictConvexSpace {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedField 𝕜] [PartialOrder 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [StrictConvexSpace 𝕜 F] (f : E →ₗᵢ[𝕜] F) : StrictConvexSpace 𝕜 E

@[instance 900]

instance Submodule.instStrictConvexSpace {𝕜 : Type u_1} {E : Type u_2} [NormedField 𝕜] [PartialOrder 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [StrictConvexSpace 𝕜 E] (p : Submodule 𝕜 E) : StrictConvexSpace 𝕜 ↥p

A vector subspace of a strict convex space is a strict convex space.

This instance has priority 900 to make sure that instances like LinearIsometry.strictConvexSpace_range are tried before this one.