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