translate_preimage_left — Mathlib

English

If s is convex in E, then the preimage under the translation map x ↦ x + z is convex for any z ∈ E. Since (x ↦ x+z) is a translation, this is just the translation of the previous statement.

Русский

Если $s$ выпукло в $E$, то предобраз под отображением переноса $x\mapsto x+z$ выпукл; для любого $z\in E$.

LaTeX

$$$\operatorname{Convex}_\mathbb{K}\bigl(\{x \in E \mid x+z \in s\}\bigr),$ для любого $z\in E$ и выпуклого $s$.$$

Lean4

/-- The translation of a convex set is also convex. -/
theorem translate_preimage_left (hs : Convex 𝕜 s) (z : E) : Convex 𝕜 ((fun x => x + z) ⁻¹' s) := by
  simpa only [add_comm] using hs.translate_preimage_right z

Похожие утверждения