comp_continuous — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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