English
For a nonempty compact set K and a function f continuous on K, for every y in the order, sSup of the image f''K is below y iff every point of K maps below y.
Русский
Для непустого компактного множества K и непрерывной на K функции f верхняя грань образа f''K лежит под y тогда и только тогда, когда каждый x ∈ K удовлетворяет f(x) < y.
LaTeX
$$$\\forall y:\\, sSup(f''K) < y \\iff \\forall x \\in K:\\, f(x) < y$$$
Lean4
theorem sSup_lt_iff_of_continuous [ClosedIciTopology α] {f : β → α} {K : Set β} (hK : IsCompact K) (h0K : K.Nonempty)
(hf : ContinuousOn f K) (y : α) : sSup (f '' K) < y ↔ ∀ x ∈ K, f x < y :=
by
refine ⟨fun h x hx => (le_csSup (hK.bddAbove_image hf) <| mem_image_of_mem f hx).trans_lt h, fun h => ?_⟩
obtain ⟨x, hx, h2x⟩ := hK.exists_isMaxOn h0K hf
refine (csSup_le (h0K.image f) ?_).trans_lt (h x hx)
rintro _ ⟨x', hx', rfl⟩; exact h2x hx'
