English
If a function has a local maximum on a set at a, and is continuous on closure, then it preserves a local maximum at a in closure.
Русский
Если функция достигает локального максимума на множестве в точке a и непрерывна на замкнутости, то максимум сохраняется в closure.
LaTeX
$$IsLocalMaxOn f s a → ContinuousOn f (closure s) → IsLocalMaxOn f (closure s) a.$$
Lean4
protected theorem closure (h : IsLocalMaxOn f s a) (hc : ContinuousOn f (closure s)) : IsLocalMaxOn f (closure s) a :=
by
rcases mem_nhdsWithin.1 h with ⟨U, Uo, aU, hU⟩
refine mem_nhdsWithin.2 ⟨U, Uo, aU, ?_⟩
rintro x ⟨hxU, hxs⟩
refine ContinuousWithinAt.closure_le ?_ ?_ continuousWithinAt_const hU
· rwa [mem_closure_iff_nhdsWithin_neBot, nhdsWithin_inter_of_mem, ← mem_closure_iff_nhdsWithin_neBot]
exact nhdsWithin_le_nhds (Uo.mem_nhds hxU)
· exact (hc _ hxs).mono (inter_subset_right.trans subset_closure)
