English
Let s1 and s2 be finite sets with s1 ⊆ s2 and s1 nonempty. Then for any f : β → α, the supremum over s1 is less than or equal to the supremum over s2, i.e., sup_{x∈s1} f(x) ≤ sup_{x∈s2} f(x).
Русский
Пусть s1 и s2 — конечные множества с включением s1 ⊆ s2 и s1 ≠ ∅. Тогда для любой функции f: β → α выполняется sup_{x∈s1} f(x) ≤ sup_{x∈s2} f(x).
LaTeX
$$$\\displaystyle \\sup_{x \\in s_1} f(x) \\le \\sup_{x \\in s_2} f(x) \\quad\\text{whenever } s_1 \\subseteq s_2\\text{ and } s_1 \\neq \\varnothing.$$$
Lean4
@[gcongr]
theorem sup'_mono {s₁ s₂ : Finset β} (h : s₁ ⊆ s₂) (h₁ : s₁.Nonempty) : s₁.sup' h₁ f ≤ s₂.sup' (h₁.mono h) f :=
Finset.sup'_le h₁ _ (fun _ hb => le_sup' _ (h hb))
