English
Let f be continuous on [a,b] with a<b and f(a)=f(b). Then there exists c ∈ (a,b) such that f attains an extremum on [a,b] at c.
Русский
Пусть f непрерывна на [a,b], a<b и f(a)=f(b). Тогда существует c ∈ (a,b), такое что f достигает экстремума на [a,b] в точке c.
LaTeX
$$$\\exists c\\in (a,b),\\; \\text{IsExtrOn}(f,[a,b],c)$$$
Lean4
/-- A continuous function on a closed interval with `f a = f b`
takes either its maximum or its minimum value at a point in the interior of the interval. -/
theorem exists_Ioo_extr_on_Icc (hab : a < b) (hfc : ContinuousOn f (Icc a b)) (hfI : f a = f b) :
∃ c ∈ Ioo a b, IsExtrOn f (Icc a b) c :=
by
have ne : (Icc a b).Nonempty :=
nonempty_Icc.2
(le_of_lt hab)
-- Consider absolute min and max points
obtain ⟨c, cmem, cle⟩ : ∃ c ∈ Icc a b, ∀ x ∈ Icc a b, f c ≤ f x := isCompact_Icc.exists_isMinOn ne hfc
obtain ⟨C, Cmem, Cge⟩ : ∃ C ∈ Icc a b, ∀ x ∈ Icc a b, f x ≤ f C := isCompact_Icc.exists_isMaxOn ne hfc
by_cases hc : f c = f a
· by_cases hC : f C = f a
· have : ∀ x ∈ Icc a b, f x = f a := fun x hx =>
le_antisymm (hC ▸ Cge x hx)
(hc ▸ cle x hx)
-- `f` is a constant, so we can take any point in `Ioo a b`
rcases nonempty_Ioo.2 hab with ⟨c', hc'⟩
refine ⟨c', hc', Or.inl fun x hx ↦ ?_⟩
simp only [mem_setOf_eq, this x hx, this c' (Ioo_subset_Icc_self hc'), le_rfl]
· refine ⟨C, ⟨lt_of_le_of_ne Cmem.1 <| mt ?_ hC, lt_of_le_of_ne Cmem.2 <| mt ?_ hC⟩, Or.inr Cge⟩
exacts [fun h => by rw [h], fun h => by rw [h, hfI]]
· refine ⟨c, ⟨lt_of_le_of_ne cmem.1 <| mt ?_ hc, lt_of_le_of_ne cmem.2 <| mt ?_ hc⟩, Or.inl cle⟩
exacts [fun h => by rw [h], fun h => by rw [h, hfI]]
