English
The preimage of a strictly convex set under a suitable linear map is strictly convex.
Русский
Обратное изображение строго выпуклого множества под подходящим линейным отображением является строго выпуклым.
LaTeX
$$$\StrictConvex 𝕜 s \Rightarrow \forall c, \StrictConvex 𝕜 (Set.preimage (fun z => c \cdot z) s)$$$
Lean4
theorem preimage_smul (hs : StrictConvex 𝕜 s) (c : 𝕜) : StrictConvex 𝕜 ((fun z => c • z) ⁻¹' s) := by
classical
obtain rfl | hc := eq_or_ne c 0
· simp_rw [zero_smul, preimage_const]
split_ifs
· exact strictConvex_univ
· exact strictConvex_empty
refine hs.linear_preimage (LinearMap.lsmul _ _ c) ?_ (smul_right_injective E hc)
unfold LinearMap.lsmul LinearMap.mk₂ LinearMap.mk₂' LinearMap.mk₂'ₛₗ
exact continuous_const_smul _
