English
If f is continuous on Ioo(a,b) and tends to the same limit l at the ends, then there is an interior extremum on Ioo a b.
Русский
Если f непрерывна на Ioo(a,b) и стремится к одному пределу l на концах, то в Ioo(a,b) существует внутри экстремум.
LaTeX
$$$\\exists c\\in Ioo(a,b),\\; \\text{IsExtrOn}(f,Ioo(a,b),c)$$$
Lean4
/-- If a function `f` is continuous on an open interval
and tends to the same value at its endpoints, then it has an extremum on this open interval. -/
theorem exists_isExtrOn_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, IsExtrOn f (Ioo a b) c :=
by
have h : EqOn (extendFrom (Ioo a b) f) f (Ioo a b) := extendFrom_extends hfc
obtain ⟨c, hc, hfc⟩ : ∃ c ∈ Ioo a b, IsExtrOn (extendFrom (Ioo a b) f) (Icc a b) c :=
exists_Ioo_extr_on_Icc hab (continuousOn_Icc_extendFrom_Ioo hab.ne hfc ha hb)
((eq_lim_at_left_extendFrom_Ioo hab ha).trans (eq_lim_at_right_extendFrom_Ioo hab hb).symm)
exact ⟨c, hc, (hfc.on_subset Ioo_subset_Icc_self).congr h (h hc)⟩
