sup_mono_fun — Mathlib

English

If f ≤ g pointwise on s, then the supremum of f over s is less than or equal to the supremum of g over s.

Русский

Если для всех элементов i ∈ s выполняется f(i) ≤ g(i), то sup_s f ≤ sup_s g.

LaTeX

$$$\displaystyle (\forall b \in s),\ f(b) \le g(b) \quad\Rightarrow\quad s.sup f \le s.sup g$$$

Lean4

@[gcongr]
theorem sup_mono_fun {g : β → α} (h : ∀ b ∈ s, f b ≤ g b) : s.sup f ≤ s.sup g :=
  Finset.sup_le fun b hb => le_trans (h b hb) (le_sup hb)

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