csInf_image_le — Mathlib

English

A dual version of the previous monotone csInf_image_le, using order dual and WithTop.

Русский

Двойственная версия предыдущего утверждения, через двойственный порядок и WithTop.

LaTeX

$$$\text{Monotone } f\;\Rightarrow\; \text{dual form of inequality for } sInf(f''s) \le f(c)$$$

Lean4

theorem csInf_image_le {s : Set α} {c : α} (hcs : c ∈ s) (h_bdd : BddBelow s) : sInf (f '' s) ≤ f c :=
  by
  let f' : αᵒᵈ → βᵒᵈ := f
  exact le_csSup_image (α := αᵒᵈ) (β := βᵒᵈ) (show Monotone f' from fun x y hxy => h_mono hxy) hcs h_bdd

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