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