Theorems · Theorem · functional analysis

IsLocalMaxOn.norm_add_sameRay

∀ {X : Type u_2} {E : Type u_3} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : TopologicalSpace X] {f : X → E} {s : Set X} {c : X} {y : E},
  IsLocalMaxOn (norm ∘ f) s c → SameRay ℝ (f c) y → IsLocalMaxOn (fun x => ‖f x + y‖) s c

If f : α → E is a function such that norm ∘ f has a local 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 local maximum on s at c.

Defined in

Mathlib.Analysis.Normed.Module.Extr

Cited by

0 results in Mathlib

Foundations

Depth 160 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SeminormedAddCommGroupNormedSpaceTopologicalSpace