pred_ofAdd — Mathlib

English

If X is a preorder with SuccOrder and IsSuccArchimedean X, then Multiplicative X is IsSuccArchimedean.

Русский

Если X — предorder с SuccOrder и IsSuccArchimedean X, то Multiplicative X является IsSuccArchimedean.

LaTeX

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

Lean4

@[simp]
theorem pred_ofAdd [Preorder X] [PredOrder X] (x : X) : pred (ofAdd x) = ofAdd (pred x) :=
  rfl

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