of_locallyFiniteOrder — Mathlib

English

Any locally finite linear additive group is Archimedean.

Русский

Любая локально конечная линейно упорядоченная аддитивная группа архимедова.

LaTeX

$$$ \text{LocallyFiniteOrder}(G) \Rightarrow \text{Archimedean}(G). $$$

Lean4

/-- Any locally finite linear additive group is archimedean. -/
theorem of_locallyFiniteOrder {G : Type*} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G]
    [LocallyFiniteOrder G] : Archimedean G :=
  .comap (LocallyFiniteOrder.addMonoidHom G) LocallyFiniteOrder.orderAddMonoidHom_strictMono

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