English
Let δ be a topological space, s a set, g: δ → α, and b ∈ s. If f has a local minimum on t at g(b) and g is continuous on s, then f ∘ g has a local minimum on s at b.
Русский
Пусть δ — топологическое пространство, s — множество, \(g: δ \to α\), и \(b \in s\). Если \(f\) имеет локальный минимум на \(t\) в точке \(g(b)\) и \(g\) непрерывна на \(s\), то \(f\\circ g\) имеет локальный минимум на \(s\) в \(b\).
LaTeX
$$$\\IsLocalMin f (g\\, b) \\Rightarrow \\text{ContinuousOn}(g,s) \\Rightarrow \\IsLocalMinOn (f \\circ g) s b$$$
Lean4
theorem comp_continuousOn [TopologicalSpace δ] {s : Set δ} {g : δ → α} {b : δ} (hf : IsLocalMin f (g b))
(hg : ContinuousOn g s) (hb : b ∈ s) : IsLocalMinOn (f ∘ g) s b :=
hf.comp_tendsto (hg b hb)
