comp_continuous — Mathlib

English

Let δ be a topological space and g: δ → α. If f is a local extreme (either min or max) at g(b) and g is continuous at b, then f ∘ g has a local extreme at b.

Русский

Пусть δ – топологическое пространство и $g: δ \to α$. Если в точке $g(b)$ у функции $f$ есть локальный экстремум (минус или максимум), и $g$ непрерывна в $b$, то $f\\circ g$ имеет локальный экстремум в $b$.

LaTeX

$$$\\IsLocalExtr f (g\\, b) \\land \\text{ContinuousAt}(g,b) \\Rightarrow \\IsLocalExtr (f \\circ g) b$$$

Lean4

theorem comp_continuous [TopologicalSpace δ] {g : δ → α} {b : δ} (hf : IsLocalExtr f (g b)) (hg : ContinuousAt g b) :
    IsLocalExtr (f ∘ g) b :=
  hf.comp_tendsto hg

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