IsGreatest — Mathlib

English

IsGreatest(s,a) means a ∈ s and a is an upper bound of s; i.e., a is the greatest element of s if it lies in s and is ≥ every element of s.

Русский

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

LaTeX

$$$ IsGreatest(s,a) \\iff (a \\in s) \\land (a \\in \\operatorname{upperBounds}(s))$$$

Lean4

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

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