IsLUB — Mathlib

English

IsLUB(s,a) means a is a least upper bound of s; equivalently, a is the least element among the upper bounds of s.

Русский

IsLUB(s,a) означает, что a является наименьшей верхней гранью множества s; то есть a — наименьшее среди верхних границ s.

LaTeX

$$$ IsLUB(s) (a) \\iff IsLeast(\\operatorname{upperBounds}(s), a)$$$

Lean4

/-- `a` is a least upper bound of a set `s`; for a partial order, it is unique if exists. -/
def IsLUB (s : Set α) : α → Prop :=
  IsLeast (upperBounds s)

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