English
If s is strictly convex, translating it by z yields a strictly convex set of the translated image.
Русский
Перемещение множества по вектору z сохраняет строгое выпуклость в образе.
LaTeX
$$$StrictConvex 𝕜 s \Rightarrow \forall z:\
E, StrictConvex 𝕜 ((fun x => z + x) '' s)$$$
Lean4
theorem add (hs : StrictConvex 𝕜 s) (ht : StrictConvex 𝕜 t) : StrictConvex 𝕜 (s + t) :=
by
rintro _ ⟨v, hv, w, hw, rfl⟩ _ ⟨x, hx, y, hy, rfl⟩ h a b ha hb hab
rw [smul_add, smul_add, add_add_add_comm]
obtain rfl | hvx := eq_or_ne v x
· refine interior_mono (add_subset_add (singleton_subset_iff.2 hv) Subset.rfl) ?_
rw [Convex.combo_self hab, singleton_add]
exact (isOpenMap_add_left _).image_interior_subset _ (mem_image_of_mem _ <| ht hw hy (ne_of_apply_ne _ h) ha hb hab)
exact subset_interior_add_left (add_mem_add (hs hv hx hvx ha hb hab) <| ht.convex hw hy ha.le hb.le hab)
