le_sSup_image_Icc — Mathlib

English

Let f be continuous on the closed interval Icc(a, b). If c ∈ Icc(a, b) then f(c) ≤ sSup{ f(x) : x ∈ Icc(a,b) }.

Русский

Пусть f непрерывна на замкнутом интервале Icc(a, b). Для C, принадлежащего Icc(a, b), выполняется f(C) ≤ sup{ f(x) : x ∈ Icc(a, b) }.

LaTeX

$$$ f(c) \le \operatorname{sSup} \{ f(x) : x \in Icc(a,b) \} $$$

Lean4

theorem le_sSup_image_Icc (h : ContinuousOn f <| Icc a b) (hc : c ∈ Icc a b) : f c ≤ sSup (f '' Icc a b) :=
  by
  have := mem_image_of_mem f hc
  rw [h.image_Icc (hc.1.trans hc.2)] at this
  exact this.2

Похожие утверждения