isGLB_Ioi — Mathlib

English

If a is a predecessor-prelimit, then (Ioi a, a) is a GLB pair; that is, a is the greatest lower bound of the open ray to the right of a.

Русский

Если a является пред-предпредельным, то (Ioi a, a) образует GLB; то есть a является наибольшей нижней границей множества x > a.

LaTeX

$$IsPredPrelimit\\ a \\to IsGLB\\ (Ioi\\ a)\\ a$$

Lean4

theorem isGLB_Ioi (ha : IsPredPrelimit a) : IsGLB (Ioi a) a :=
  ha.dual.isLUB_Iio

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