inf — Mathlib

English

For a finite set s and a function f on its elements, the infimum of f over s is the infimum of the values f(b) for b ∈ s; i.e., inf over s { f(b) } = ⊓_{b∈s} f(b).

Русский

Для конечного множества s и функции f на его элементах наименьшее значение инфимума от f над s равно инфимума от значений f(b) по b ∈ s: inf_{b∈s} f(b).

LaTeX

$$$ s.inf f = \inf_{b \in s} f(b) $$$

Lean4

/-- Infimum of a finite set: `inf {a, b, c} f = f a ⊓ f b ⊓ f c` -/
def inf (s : Finset β) (f : β → α) : α :=
  s.fold (· ⊓ ·) ⊤ f

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