English
In a linearly ordered Archimedean additive group, discreteness (existence of an order isomorphism to ℤ) holds exactly when the order is not densely ordered.
Русский
В линейно упорядоченной архимедовой аддитивной группе дискретность эквивалентна тому, что порядок не является плотно упорядоченным.
LaTeX
$$$(\exists \phi: G \cong_o \mathbb{Z}) \;\leftrightarrow\; \lnot \mathrm{DenselyOrdered}(G)$$$
Lean4
/-- Any linearly ordered archimedean additive group is either isomorphic (and order-isomorphic)
to the integers, or is densely ordered, exclusively. -/
theorem discrete_iff_not_denselyOrdered (G : Type*) [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G]
[Archimedean G] : Nonempty (G ≃+o ℤ) ↔ ¬DenselyOrdered G :=
by
suffices ∀ (_ : G ≃+o ℤ), ¬DenselyOrdered G
by
rcases LinearOrderedAddCommGroup.discrete_or_denselyOrdered G with ⟨⟨h⟩⟩ | h
· simpa [this h] using ⟨h⟩
· simp only [h, not_true_eq_false, iff_false, not_nonempty_iff]
exact ⟨fun H ↦ (this H) h⟩
intro e H
rw [denselyOrdered_iff_of_orderIsoClass e] at H
obtain ⟨_, _⟩ := exists_between (one_pos (α := ℤ))
cutsat
