sup — Mathlib

English

The supremum over a finite set s of a function f is the join of the values f(b) for b in s: sup_{b∈s} f(b) = ⋁_{b∈s} f(b).

Русский

Наивысшая грань над функцией f на конечном множестве s равна объединению значений f(b) по b∈s: sup_{b∈s} f(b) = ⋁_{b∈s} f(b).

LaTeX

$$$ \\sup_{b \\in s} f(b) = \\bigvee_{b \\in s} f(b) $$$

Lean4

/-- Supremum of a finite set: `sup {a, b, c} f = f a ⊔ f b ⊔ f c` -/
def sup (s : Finset β) (f : β → α) : α :=
  s.fold (· ⊔ ·) ⊥ f

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