English
If f is continuous on Ioo(a,b) and tends to the same limit l at both ends, then there exists c ∈ Ioo(a,b) with IsLocalExtr f c.
Русский
Если f непрерывна на Ioo(a,b) и имеет одинаковый предел в концах, то существует c ∈ Ioo(a,b), где f имеет локальный экстремум.
LaTeX
$$$\\exists c\\in Ioo(a,b),\\; \\text{IsLocalExtr}(f,c)$$$
Lean4
/-- If a function `f` is continuous on an open interval
and tends to the same value at its endpoints,
then it has a local extremum on this open interval. -/
theorem exists_isLocalExtr_Ioo_of_tendsto (hab : a < b) (hfc : ContinuousOn f (Ioo a b)) (ha : Tendsto f (𝓝[>] a) (𝓝 l))
(hb : Tendsto f (𝓝[<] b) (𝓝 l)) : ∃ c ∈ Ioo a b, IsLocalExtr f c :=
let ⟨c, cmem, hc⟩ := exists_isExtrOn_Ioo_of_tendsto hab hfc ha hb
⟨c, cmem, hc.isLocalExtr <| Ioo_mem_nhds cmem.1 cmem.2⟩
