English
Let R be a nonunital star-ordered ring. An element x ∈ R is positive (x > 0) if and only if x ≠ 0 and x lies in the additive submonoid closure of the set {star(s) · s : s ∈ R}. Equivalently, 0 < x iff x ≠ 0 and x ∈ AddSubmonoid.closure(Set.range(s ↦ star s · s)).
Русский
Пусть R является ненулевым звездоупорядоченным кольцом. Элемент x ∈ R положителен (x > 0) тогда и только тогда, когда x ≠ 0 и x принадлежит замкнутому по сложению подмоноиду множества {star(s) · s : s ∈ R}. Эквивалентно: 0 < x тогда и только тогда, когда x ≠ 0 и x ∈ AddSubmonoid.closure(Set.range(λ s, star s · s)).
LaTeX
$$$0 < x \iff x \neq 0 \land x \in \operatorname{AddSubmonoid.closure}\big(\operatorname{Set.range}(\lambda s:R, \star s \cdot s)\big)$$$
Lean4
theorem pos_iff : 0 < x ↔ x ≠ 0 ∧ x ∈ AddSubmonoid.closure (Set.range fun s : R => star s * s) := by
simp [lt_iff_le_and_ne, and_comm, eq_comm, le_iff]
