English
Let R be a star-ordered ring. For any x,y ∈ R, x < y holds if and only if there exists a nonzero p belonging to the additive submonoid closed range of star(s)·s such that y = x + p.
Русский
Пусть R — звездоупорядоченное кольцо. Для любых x,y ∈ R верно: x < y тогда и только тогда, когда существует p ≠ 0 с p ∈ AddSubmonoid.closure(Set.range(star s · s)) и y = x + p.
LaTeX
$$$x < y \iff \exists p \neq 0,\ p \in \operatorname{AddSubmonoid.closure}\big(\operatorname{Set.range}(\lambda s:R, \star s \cdot s)\big) \land y = x + p$$$
Lean4
theorem lt_iff : x < y ↔ ∃ p ≠ 0, p ∈ AddSubmonoid.closure (Set.range fun s => star s * s) ∧ y = x + p :=
by
rw [lt_iff_le_and_ne, and_comm, StarOrderedRing.le_iff, ← exists_and_left]
congr! 2 with p
simp +contextual [← and_assoc]
