English
If f: α → E has a maximum of ‖f‖ along a filter l at c, then the function x ↦ ‖f(x) + f(c)‖ also attains a maximum along l at c.
Русский
Если у функции f: α → E максимум нормы ‖f‖ вдоль фильтра l в точке c, то функция x ↦ ‖f(x) + f(c)‖ также достигает максимума по l в c.
LaTeX
$$$\\text{IsMaxFilter}(\\|f\\| \\circ f, l, c) \\Rightarrow \\text{IsMaxFilter}(\\lambda x. \\|f(x) + f(c)\\|, l, c)$$$
Lean4
/-- If `f : α → E` is a function such that `norm ∘ f` has a maximum along a filter `l` at a point
`c`, then the function `fun x => ‖f x + f c‖` has a maximum along `l` at `c`. -/
theorem norm_add_self (h : IsMaxFilter (norm ∘ f) l c) : IsMaxFilter (fun x => ‖f x + f c‖) l c :=
IsMaxFilter.norm_add_sameRay h SameRay.rfl
