IsUpperSet — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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