IsLowerSet — Mathlib

English

A subset s of α is a lower set if whenever b ≤ a and a ∈ s, then b ∈ s.

Русский

Подмножество s до α является нижним множеством, если для любого b ≤ a и a ∈ s следует b ∈ s.

LaTeX

$$$\\\\operatorname{IsLowerSet}(s) \\\\Leftrightarrow \\\\forall a,b, \\\\ b \\\\le a \\\\Rightarrow a \\\\in s \\\\Rightarrow b \\\\in s.$$$

Lean4

/-- A lower set in an order `α` is a set such that any element less than one of its members is also
a member. Also called down-set, downward-closed set. -/
def IsLowerSet {α : Type*} [LE α] (s : Set α) : Prop :=
  ∀ ⦃a b : α⦄, b ≤ a → a ∈ s → b ∈ s

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