norm_add_self — Mathlib

English

If f: α → E has a maximum on a set s at c for the norm, then x ↦ ‖f(x) + f(c)‖ also attains a maximum at c on s.

Русский

Если у f: α → E максимум нормы на множестве s в точке c, то x ↦ ‖f(x) + f(c)‖ тоже имеет максимум на s в c.

LaTeX

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

Lean4

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

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