discrete_iff_not_denselyOrdered — Mathlib

English

For a linearly ordered additive group with Archimedean property, there exists an order isomorphism to ℤ if and only if the order is not densely ordered.

Русский

Для линейно упорядоченной архимедовой аддитивной группы существует упорядочимое изоморождение с ℤ тогда и только тогда, когда порядок не плотно упорядочен.

LaTeX

$$$(\exists \phi: G \cong_o \mathbb{Z}) \iff \lnot \mathrm{DenselyOrdered}(G)$$$

Lean4

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

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