English
An upper set relative to a predicate P is a set s such that every a ∈ s satisfies P a, and whenever a ≤ b and P b holds, then b ∈ s.
Русский
Верхнее множество относительно предиката P — множество s, такое что для каждого a ∈ s выполняется P(a), и если a ≤ b и P(b) верно, то b ∈ s.
LaTeX
$$$\\\\operatorname{IsRelUpperSet}(s,P) \\\\Leftrightarrow \\\\forall a, a \\in s \rightarrow P(a) \\land \\\\forall b, a \\le b \\rightarrow P(b) \\rightarrow b \\in s.$$$
Lean4
/-- An upper set relative to a predicate `P` is a set such that all elements satisfy `P` and
any element greater than one of its members and satisfying `P` is also a member. -/
def IsRelUpperSet {α : Type*} [LE α] (s : Set α) (P : α → Prop) : Prop :=
∀ ⦃a : α⦄, a ∈ s → P a ∧ ∀ ⦃b : α⦄, a ≤ b → P b → b ∈ s
