English
To define a StarOrderedRing structure it suffices to verify that x ≤ y holds exactly when y = x + star(s)·s for some s.
Русский
Чтобы задать структуру StarOrderedRing достаточно показать, что x ≤ y эквивалентно существованию s с равенством y = x + star(s)·s.
LaTeX
$$$\\\\forall x,y \\\\in R, \\\\le x y \\\\Leftrightarrow \\\\exists s, \\\\ y = x + \\star(s) \\cdot s.$$$
Lean4
/-- To construct a `StarOrderedRing` instance it suffices to show that `x ≤ y` if and only if
`y = x + star s * s` for some `s : R`.
This is provided for convenience because it holds in some common scenarios (e.g.,`ℝ≥0`, `C(X, ℝ≥0)`)
and obviates the hassle of `AddSubmonoid.closure_induction` when creating those instances.
If you are working with a `NonUnitalRing` and not a `NonUnitalSemiring`, see
`StarOrderedRing.of_nonneg_iff` for a more convenient version.
-/
theorem of_le_iff (h_le_iff : ∀ x y : R, x ≤ y ↔ ∃ s, y = x + star s * s) : StarOrderedRing R where
le_iff x
y := by
refine ⟨fun h => ?_, ?_⟩
· obtain ⟨p, hp⟩ := (h_le_iff x y).mp h
exact ⟨star p * p, AddSubmonoid.subset_closure ⟨p, rfl⟩, hp⟩
· rintro ⟨p, hp, hpxy⟩
revert x y hpxy
refine AddSubmonoid.closure_induction ?_ (fun x y h => add_zero x ▸ h.ge) ?_ hp
· rintro _ ⟨s, rfl⟩ x y rfl
exact (h_le_iff _ _).mpr ⟨s, rfl⟩
· rintro _ _ _ _ ha hb x y rfl
rw [← add_assoc]
exact (ha _ _ rfl).trans (hb _ _ rfl)
