English
For a linearly ordered multiplicative group G, the ray {x ≥ g} with the strict order is well-founded if and only if G is order-isomorphic to the multiplicative integers ℤᵐ⁰.
Русский
Для линейно упорядоченной мультипликативной группы G луч {x ≥ g} с отношением < хорошо упорядован тогда и только тогда, когда G упорядочимо изоморфен мультипликативным целым ℤᵐ⁰.
LaTeX
$$$\text{WellFoundedOn} \{x : G \mid g \le x\} (<) \;\iff\; \exists \phi: G \cong_* o \mathbb{Z}^{\mathbf{m0}}$$$
Lean4
theorem wellFoundedOn_setOf_le_lt_iff_nonempty_discrete {G : Type*} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G]
[Nontrivial G] {g : G} : Set.WellFoundedOn {x : G | g ≤ x} (· < ·) ↔ Nonempty (G ≃*o Multiplicative ℤ) :=
by
let e : G ≃o Additive G := OrderIso.refl G
suffices Set.WellFoundedOn {x : G | g ≤ x} (· < ·) ↔ Set.WellFoundedOn {x | e g ≤ x} (· < ·) by
rw [this, LinearOrderedAddCommGroup.wellFoundedOn_setOf_le_lt_iff_nonempty_discrete,
OrderAddMonoidIso.toMultiplicativeRight.nonempty_congr]
refine ⟨fun h ↦ (h.mapsTo e.symm fun _ ↦ e.le_symm_apply.mpr).mono' ?_, fun h ↦ (h.mapsTo e fun _ ↦ ?_).mono' ?_⟩ <;>
simp [Function.onFun]
