translate_left — Mathlib

English

Left translation preserves strict convexity.

Русский

Левый перенос сохраняет строгую выпуклость.

LaTeX

$$$StrictConvexOn\ 𝕜\ s\ f \Rightarrow \forall c\, StrictConvexOn\ 𝕜\ (Set.preimage(\lambda z. z+c)\ s)\ (f \circ (\lambda z. z+c))$$$

Lean4

/-- Left translation preserves strict convexity. -/
theorem translate_left (hf : StrictConvexOn 𝕜 s f) (c : E) :
    StrictConvexOn 𝕜 ((fun z => c + z) ⁻¹' s) (f ∘ fun z => z + c) := by
  simpa only [add_comm] using hf.translate_right c

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