unique — Mathlib

English

If Ha : IsGLB s a and Hb : IsGLB s b, then a = b. The greatest lower bound, when it exists, is unique.

Русский

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

LaTeX

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

Lean4

theorem unique (Ha : IsGLB s a) (Hb : IsGLB s b) : a = b :=
  IsGreatest.unique Ha Hb

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