English
Let t ⊆ α, s ⊆ δ, g: δ → α. If f has a local maximum on t at g(b) and s ⊆ g^{-1}(t) with ContinuousOn g on s, then f ∘ g has a local maximum on s at b.
Русский
Пусть t ⊆ α, s ⊆ δ, \(g: δ \to α\). Если у f локальный максимум на t в точке \(g(b)\) и \(s \subseteq g^{-1}(t)\) с непрерывностью \(g\) на \(s\), тогда \(f\\circ g\) имеет локальный максимум на \(s\) в \(b\).
LaTeX
$$$\\IsLocalMaxOn f t (g b) \\land (s \\subseteq g^{-1} t) \\land \\text{ContinuousOn } g s \\Rightarrow \\IsLocalMaxOn (f \\circ g) s b$$$
Lean4
theorem comp_continuousOn [TopologicalSpace δ] {t : Set α} {s : Set δ} {g : δ → α} {b : δ} (hf : IsLocalMaxOn f t (g b))
(hst : s ⊆ g ⁻¹' t) (hg : ContinuousOn g s) (hb : b ∈ s) : IsLocalMaxOn (f ∘ g) s b :=
hf.comp_tendsto
(tendsto_nhdsWithin_mono_right (image_subset_iff.mpr hst) (ContinuousWithinAt.tendsto_nhdsWithin_image (hg b hb)))
