norm_add_self — Mathlib

English

If f: X → E has a local maximum of ‖f‖ at c, then x ↦ ‖f(x) + f(c)‖ has a local maximum at c.

Русский

Если у f: X → E есть локальный максимум по норме в точке c, тогда x ↦ ‖f(x) + f(c)‖ имеет локальный максимум в c.

LaTeX

$$$\\text{IsLocalMaxOn}(\\|f\\| \\circ f, s, c) \\Rightarrow \\text{IsLocalMaxOn}(\\lambda x. \\|f(x) + f(c)\\|, s, c)$$$

Lean4

/-- If `f : α → E` is a function such that `norm ∘ f` has a local maximum on a set `s` at a point
`c`, then the function `fun x => ‖f x + f c‖` has a local maximum on `s` at `c`. -/
theorem norm_add_self (h : IsLocalMaxOn (norm ∘ f) s c) : IsLocalMaxOn (fun x => ‖f x + f c‖) s c :=
  IsMaxFilter.norm_add_self h

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