English
Let δ be a topological space, t a set of α, g: δ → α, b ∈ δ. If f has a local extr at g(b) on t, and g is continuous on a set s with b ∈ s, then f ∘ g has a local extr on s at b.
Русский
Пусть δ — топологическое пространство, t ⊆ α, \(g: δ \to α\), \(b \in δ\). Если у \(f\) есть локальный экстремум в точке \(g(b)\) на \(t\), и \(g\) непрерывна на множествах, содержащих \(b\), то \(f\\circ g\) имеет локальный экстремум на \(s\) в \(b\).
LaTeX
$$$\\IsLocalExtr f t (g b) \\Rightarrow (s\\subseteq g^{-1}(t)) \\Rightarrow (\\text{ContinuousOn } g s) \\Rightarrow (b \\in s) \\Rightarrow \\IsLocalExtrOn (f \\circ g) s b$$$
Lean4
theorem comp_continuousOn [TopologicalSpace δ] {s : Set δ} (g : δ → α) {b : δ} (hf : IsLocalExtr f (g b))
(hg : ContinuousOn g s) (hb : b ∈ s) : IsLocalExtrOn (f ∘ g) s b :=
hf.elim (fun hf => (hf.comp_continuousOn hg hb).isExtr) fun hf => (IsLocalMax.comp_continuousOn hf hg hb).isExtr
