English
If f: α → E is such that the norm of f attains a maximum along a filter l at c, and y lies on the same ray as f(c), then the function x ↦ ‖f(x) + y‖ also attains a maximum along l at c.
Русский
Если функция f: α → E имеет максимум по норме вдоль фильтра l в точке c, и вектор y лежит на том же луче, что и f(c), тогда функция x ↦ ‖f(x) + y‖ тоже достигает максимума по l в c.
LaTeX
$$$\\text{IsMaxFilter}(\\|f\\| \\circ f, l, c) \\; \\land \\; \\text{SameRay}(f(c), y) \\Rightarrow \\text{IsMaxFilter}(\\lambda x. \\|f(x) + y\\|, l, c)$$$
Lean4
/-- If `f : α → E` is a function such that `norm ∘ f` has a maximum along a filter `l` 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 along `l` at `c`. -/
theorem norm_add_sameRay (h : IsMaxFilter (norm ∘ f) l c) (hy : SameRay ℝ (f c) y) :
IsMaxFilter (fun x => ‖f x + y‖) l c :=
h.mono fun x hx =>
calc
‖f x + y‖ ≤ ‖f x‖ + ‖y‖ := norm_add_le _ _
_ ≤ ‖f c‖ + ‖y‖ := (add_le_add_right hx _)
_ = ‖f c + y‖ := hy.norm_add.symm
