English
Translation preserves strict convexity: translating a strictly convex set by z yields a strictly convex preimage under addition.
Русский
Перенос по вектору сохраняет строгое выпуклость: перенесение множества по z сохраняет строгое выпуклое.
LaTeX
$$$StrictConvex 𝕜 s \Rightarrow \forall z:\
E, StrictConvex 𝕜 ((fun x => z + x)^{-1} s)$$$
Lean4
/-- The translation of a strictly convex set is also strictly convex. -/
theorem preimage_add_right (hs : StrictConvex 𝕜 s) (z : E) : StrictConvex 𝕜 ((fun x => z + x) ⁻¹' s) :=
by
intro x hx y hy hxy a b ha hb hab
refine preimage_interior_subset_interior_preimage (continuous_add_left _) ?_
have h := hs hx hy ((add_right_injective _).ne hxy) ha hb hab
rwa [smul_add, smul_add, add_add_add_comm, ← _root_.add_smul, hab, one_smul] at h
