English
If s is a convex subset of a vector space E, then for any vector z ∈ E, the translated preimage {x ∈ E | z + x ∈ s} is convex. Equivalently, s is convex implies s − z is convex for every z ∈ E.
Русский
Если s — выпуклое подмножество векторного пространства E, то для любого вектора z ∈ E множество {x ∈ E | z + x ∈ s} выпукло. Эквивалентно: выпуклость сохраняется при переносе, т.е. s − z выпукло для любого z.
LaTeX
$$$\operatorname{Convex}_\mathbb{K}\bigl(\{x \in E \mid z+x \in s\}\bigr),$ где $s$ выпукло и $z\in E$.$$
Lean4
/-- The translation of a convex set is also convex. -/
theorem translate_preimage_right (hs : Convex 𝕜 s) (z : E) : Convex 𝕜 ((fun x => z + x) ⁻¹' s) :=
by
intro x hx y hy a b ha hb hab
have h := hs hx hy ha hb hab
rwa [smul_add, smul_add, add_add_add_comm, ← add_smul, hab, one_smul] at h
