IsGLB — Mathlib

English

IsGLB(s,a) means a is a greatest lower bound of s; i.e., a ∈ s and a is a greatest lower bound of s.

Русский

IsGLB(s,a) означает, что a является наибольшей нижней границей s; то есть a ∈ s и a — наибольшая нижняя граница.

LaTeX

$$$ IsGLB(s) (a) \\iff IsGreatest(\\operatorname{lowerBounds}(s), a)$$$

Lean4

/-- `a` is a greatest lower bound of a set `s`; for a partial order, it is unique if exists. -/
def IsGLB (s : Set α) : α → Prop :=
  IsGreatest (lowerBounds s)

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