sup'_mono_fun — Mathlib

English

Let s be a finite nonempty set and f,g : β → α be functions with f ≤ g pointwise on s; then the supremum of f over s is ≤ the supremum of g over s; i.e. sup'_{s} f ≤ sup'_{s} g when f(b) ≤ g(b) for all b ∈ s.

Русский

Пусть s — конечное непустое множество и функции f,g : β → α удовлетворяют f(b) ≤ g(b) для всех b ∈ s. Тогда sup'_{s} f ≤ sup'_{s} g.

LaTeX

$$$\\displaystyle \\text{If } \\forall b \\in s, \\ f(b) \\le g(b), \\text{ then } \\sup_{x \\in s} f(x) \\le \\sup_{x \\in s} g(x).$$$

Lean4

@[gcongr]
theorem sup'_mono_fun {hs : s.Nonempty} {f g : β → α} (h : ∀ b ∈ s, f b ≤ g b) : s.sup' hs f ≤ s.sup' hs g :=
  sup'_le _ _ fun b hb ↦ (h b hb).trans (le_sup' _ hb)

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