English
Let s be a finite set of β and f, g : β → α, where α is a semilattice with infimum. If for every b in s we have f(b) ≤ g(b), then the infimum of f over s is below the infimum of g over s; i.e., s.inf f ≤ s.inf g.
Русский
Пусть s — конечное множество элементов β и функции f, g : β → α, где α — полупорядоченное множество с наименьшим элементом. Если для каждого b ∈ s выполняется f(b) ≤ g(b), то инфимум по s от f не превосходит инфимум по s от g; то есть s.inf f ≤ s.inf g.
LaTeX
$$$ (\\forall b \\in s, f(b) \\le g(b)) \\Rightarrow s\\inf f \\le s\\inf g $$$
Lean4
@[gcongr]
theorem inf_mono_fun {g : β → α} (h : ∀ b ∈ s, f b ≤ g b) : s.inf f ≤ s.inf g :=
Finset.le_inf fun b hb => le_trans (inf_le hb) (h b hb)
