English
If f is continuous on Ioo(a,b) and has an interior extr point, then there exists c ∈ Ioo(a,b) with IsLocalExtr f c.
Русский
Если функция непрерывна на открытом интервале Ioo(a,b) и имеет локальный экстремум внутри, то существует c ∈ Ioo(a,b) с IsLocalExtr f c.
LaTeX
$$$\\exists c\\in Ioo(a,b),\\; \\text{IsLocalExtr}(f,c)$$$
Lean4
/-- A continuous function on a closed interval with `f a = f b`
has a local extremum at some point of the corresponding open interval. -/
theorem exists_isLocalExtr_Ioo (hab : a < b) (hfc : ContinuousOn f (Icc a b)) (hfI : f a = f b) :
∃ c ∈ Ioo a b, IsLocalExtr f c :=
let ⟨c, cmem, hc⟩ := exists_Ioo_extr_on_Icc hab hfc hfI
⟨c, cmem, hc.isLocalExtr <| Icc_mem_nhds cmem.1 cmem.2⟩
