above — Mathlib

English

For a cofinal set D and x ∈ P, above(D, x) is a chosen element of D with x ≤ above(D, x).

Русский

Для кофинального множества D и элемента x ∈ P верхнее(D, x) — выбранный элемент из D такой, что x ≤ above(D, x).

LaTeX

$$$ \text{above}(D,x) \in D \wedge x \le \text{above}(D,x). $$$

Lean4

/-- A (noncomputable) element of a cofinal set lying above a given element. -/
noncomputable def above : P :=
  Classical.choose <| D.isCofinal x

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