English
The map x ↦ star x is order-reversing or preserving depending on the context; in a star-ordered ring we have 0 ≤ star x ⇔ 0 ≤ x and star x ≤ star y ⇔ x ≤ y.
Русский
Отображение x ↦ star x сохраняет или обращает порядок в зависимости от контекста; в звездоупорядоченном кольце имеем 0 ≤ star x ⇔ 0 ≤ x и star x ≤ star y ⇔ x ≤ y.
LaTeX
$$$\text{star is order-isomorphism: } star x \le star y \iff x \le y$$$
Lean4
@[simp]
theorem star_le_star_iff {x y : R} : star x ≤ star y ↔ x ≤ y :=
by
suffices ∀ x y, x ≤ y → star x ≤ star y from ⟨by simpa only [star_star] using this (star x) (star y), this x y⟩
intro x y h
rw [StarOrderedRing.le_iff] at h ⊢
obtain ⟨d, hd, rfl⟩ := h
refine ⟨starAddEquiv d, ?_, star_add _ _⟩
refine AddMonoidHom.mclosure_preimage_le _ _ <| AddSubmonoid.closure_mono ?_ hd
rintro - ⟨s, rfl⟩
exact ⟨s, by simp⟩
