SupClosed — Mathlib

English

SupClosed s means that s is closed under finite suprema: for all a,b in s, a ⊔ b ∈ s.

Русский

SupClosed s означает, что множество s замкнуто по конечной мажорной операцией: для любых a,b∈s верно a ⊔ b ∈ s.

LaTeX

$$$$ \operatorname{SupClosed}(s) \iff \forall a\in s\,\forall b\in s\,a \sqcup b \in s $$$$

Lean4

/-- A set `s` is *sup-closed* if `a ⊔ b ∈ s` for all `a ∈ s`, `b ∈ s`. -/
def SupClosed (s : Set α) : Prop :=
  ∀ ⦃a⦄, a ∈ s → ∀ ⦃b⦄, b ∈ s → a ⊔ b ∈ s

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