comp_continuousOn — Mathlib

English

If f has a local extr on s, then its negation −f has a local extr of the opposite type on s.

Русский

Если у функции f на s есть локальный экстремум, то у −f будет экстремум противоположного типа на той же области.

LaTeX

$$$\\IsLocalExtrOn f s a \\Rightarrow \\IsLocalExtrOn (\\lambda x \\mapsto -f x) s a$$$

Lean4

theorem comp_continuousOn [TopologicalSpace δ] {t : Set α} {s : Set δ} (g : δ → α) {b : δ}
    (hf : IsLocalExtrOn f t (g b)) (hst : s ⊆ g ⁻¹' t) (hg : ContinuousOn g s) (hb : b ∈ s) :
    IsLocalExtrOn (f ∘ g) s b :=
  hf.elim (fun hf => (hf.comp_continuousOn hst hg hb).isExtr) fun hf =>
    (IsLocalMaxOn.comp_continuousOn hf hst hg hb).isExtr

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