IsLeast — Mathlib

English

IsLeast(s,a) means a ∈ s and a is a lower bound of s; i.e., a is the least element of s if it is in s and bounded below by all elements of s.

Русский

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

LaTeX

$$$ IsLeast(s,a) \\iff (a \\in s) \\land (a \\in \\operatorname{lowerBounds}(s))$$$

Lean4

/-- `a` is a least element of a set `s`; for a partial order, it is unique if exists. -/
def IsLeast (s : Set α) (a : α) : Prop :=
  a ∈ s ∧ a ∈ lowerBounds s

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