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{IsLocalMax}(\\|f\\|, c) \\Rightarrow \\text{IsLocalMax}(\\lambda x. \\|f(x) + f(c)\\|, c)$$$

Lean4

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

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