comp_continuous — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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