solidClosure — Mathlib

English

Let α be a lattice-ordered additive commutative group and s a subset of α. The solid closure of s is the smallest solid superset of s, consisting of all elements y for which there exists x ∈ s with |y| ≤ |x|.

Русский

Пусть α — это упорядоченная по частям группа с аддитивной операцией и s — подмножество α. Солидное замыкание s есть минимальное твердое (солидное) надмножество, содержащее s; то есть все элементы y такие, что существует x ∈ s с |y| ≤ |x|.

LaTeX

$$$\operatorname{solidClosure}(s) = \{ y \in \alpha \mid \exists x \in s, |y| \le |x| \}$$$

Lean4

/-- The solid closure of a subset `s` is the smallest superset of `s` that is solid. -/
def solidClosure (s : Set α) : Set α :=
  {y | ∃ x ∈ s, |y| ≤ |x|}

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