instIsSuccArchimedeanAdditive — Mathlib

English

If X is a Preorder with a SuccOrder and IsSuccArchimedean X, then the additive structure on X is IsSuccArchimedean as well.

Русский

Если X — частично упорядоченное множество с порядком следования и свойством IsSuccArchimedean, то аддитивная структура над X также имеет свойство IsSuccArchimedean.

LaTeX

$$IsSuccArchimedean X → IsSuccArchimedean (Additive X)$$

Lean4

instance [Preorder X] [SuccOrder X] [h : IsSuccArchimedean X] : IsSuccArchimedean (Additive X) :=
  h

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