instIsSuccArchimedeanMultiplicative

English

If X is a preorder with a succ-order and IsSuccArchimedean X, then Multiplicative X is IsSuccArchimedean.

Русский

Если X — предпорядок с переходом к следующему и IsSuccArchimedean X, то Multiplicative X тоже является IsSuccArchimedean.

LaTeX

$$$$\forall X\ [\text{Preorder } X] [\text{SuccOrder } X] [\text{IsSuccArchimedean } X] \Rightarrow \text{IsSuccArchimedean}(\text{Multiplicative } X)$$$$

Lean4

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

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