English
If f: α → E has a maximum of ‖f‖ on a set s at c and y lies on the same ray as f(c), then the function x ↦ ‖f(x) + y‖ also attains a maximum on s at c.
Русский
Если у функции f: α → E максимум нормы ‖f‖ на множестве s в точке c, и вектор y лежит на том же луче, что и f(c), тогда функция x ↦ ‖f(x) + y‖ тоже достигает максимума на s в c.
LaTeX
$$$\\text{IsMaxOn}(\\|f\\| \\circ f, s, c) \\land \\text{SameRay}(f(c), y) \\Rightarrow \\text{IsMaxOn}(\\lambda x. \\|f(x) + y\\|, s, c)$$$
Lean4
/-- If `f : α → E` is a function such that `norm ∘ f` has a maximum on a set `s` at a point `c` and
`y` is a vector on the same ray as `f c`, then the function `fun x => ‖f x + y‖` has a maximum
on `s` at `c`. -/
theorem norm_add_sameRay (h : IsMaxOn (norm ∘ f) s c) (hy : SameRay ℝ (f c) y) : IsMaxOn (fun x => ‖f x + y‖) s c :=
IsMaxFilter.norm_add_sameRay h hy
