IsSolid — Mathlib

English

A subset s of a lattice-ordered group is solid if whenever x ∈ s and y with |y| ≤ |x|, then y ∈ s.

Русский

Подмножество s в решётко упорядоченной группе называется солидным, если для любых x ∈ s и любого y с |y| ≤ |x| выполняется y ∈ s.

LaTeX

$$IsSolid(s) := ∀ ⦃x⦄, x ∈ s → ∀ ⦃y⦄, |y| ≤ |x| → y ∈ s$$

Lean4

/-- A set `s` in a lattice ordered group is *solid* if for all `x ∈ s` and all `y ∈ α` such that
`|y| ≤ |x|`, then `y ∈ s`. -/
def IsSolid (s : Set α) : Prop :=
  ∀ ⦃x⦄, x ∈ s → ∀ ⦃y⦄, |y| ≤ |x| → y ∈ s

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