discrete_or_denselyOrdered — Mathlib

English

Let G be a linearly ordered additive group with Archimedean property. Then either G is isomorphic to (ℤ, +) as an ordered group, or G is densely ordered.

Русский

Пусть G — линейно упорядоченная аддитивная группа с архимедовым свойством. Тогда либо G ≅ ℤ как упорядоченная группа, либо порядок на G плотный.

LaTeX

$$$\exists \phi: G \cong_o \mathbb{Z} \;\lor\; \mathrm{DenselyOrdered}(G)$$

Lean4

/-- Any linearly ordered mul-archimedean group is either isomorphic (and order-isomorphic)
to the multiplicative integers, or is densely ordered. -/
theorem discrete_or_denselyOrdered : Nonempty (G ≃*o Multiplicative ℤ) ∨ DenselyOrdered G :=
  by
  rw [← OrderAddMonoidIso.toMultiplicativeRight.nonempty_congr]
  exact LinearOrderedAddCommGroup.discrete_or_denselyOrdered (Additive G)

Похожие утверждения