unique — Mathlib

English

If a and b are both least upper bounds of a set s in a partially ordered set, then a = b. Thus the least upper bound is unique when it exists.

Русский

Если два элемента a и b являются наименьшими верхними пределами множества s в частично упорядоченном множестве, то a = b; существует единственная наименьшая верхняя грань.

LaTeX

$$$ IsLUB(s,a) \\rightarrow IsLUB(s,b) \\rightarrow a=b $$$

Lean4

theorem unique (Ha : IsLUB s a) (Hb : IsLUB s b) : a = b :=
  IsLeast.unique Ha Hb

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