le_csSup_image — Mathlib

English

If f is monotone from α to β, and c ∈ s with s nonempty and bounded below, then sInf (f'' s) ≤ f(c).

Русский

Пусть f монотонна от α к β, и c ∈ s, s непусто и ограничено снизу; тогда sInf(f'' s) ≤ f(c).

LaTeX

$$$\text{Monotone } f \Rightarrow \forall s, c, c \in s \Rightarrow BddBelow(s) \Rightarrow sInf(f''s) \le f(c)$$$

Lean4

theorem le_csSup_image {s : Set α} {c : α} (hcs : c ∈ s) (h_bdd : BddAbove s) : f c ≤ sSup (f '' s) :=
  le_csSup (map_bddAbove h_mono h_bdd) (mem_image_of_mem f hcs)

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