sInf_image_Icc_le — Mathlib

English

For a continuous function on Icc(a,b), the image's infimum over Icc lies below f(c) for any c in Icc.

Русский

Для непрерывной функции на Icc(a,b) наименьшее значение образа на Icc не превышает значение на любом фиксированном c внутри Icc.

LaTeX

$$$\\mathrm{sInf}(f''\\mathrm{Icc}(a,b)) \\le f(c) \\\\text{ for all } c \\in \\mathrm{Icc}(a,b)$$$

Lean4

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

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