English
Let G be a linearly ordered additive group that is Archimedean. Then either G is order-isomorphic to the integers, or the order on G is dense.
Русский
Пусть G — линейно упорядоченная архимедова аддитивная группа. Тогда либо существует упорядочимое изоморождение G с ℤ, либо упорядочение на G плотно упорядочено.
LaTeX
$$$\exists \phi: G \cong_o \mathbb{Z} \;\lor\; \mathrm{DenselyOrdered}(G)$$
Lean4
/-- Any linearly ordered archimedean additive group is either isomorphic (and order-isomorphic)
to the integers, or is densely ordered. -/
theorem discrete_or_denselyOrdered (G : Type*) [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] [Archimedean G] :
Nonempty (G ≃+o ℤ) ∨ DenselyOrdered G :=
by
by_cases H : ∃ x, IsLeast {y : G | 0 < y} x
· obtain ⟨x, hx⟩ := H
exact Or.inl ⟨(int_orderAddMonoidIso_of_isLeast_pos hx)⟩
· push_neg at H
refine Or.inr ⟨?_⟩
intro x y hxy
specialize H (y - x)
obtain ⟨z, hz⟩ : ∃ z : G, 0 < z ∧ z < y - x := by
contrapose! H
refine ⟨by simp [hxy], fun _ ↦ H _⟩
refine ⟨x + z, ?_, ?_⟩
· simp [hz.left]
· simpa [lt_sub_iff_add_lt'] using hz.right
