pred_toAdd — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem pred_toAdd [Preorder X] [PredOrder X] (x : Multiplicative X) : pred x.toAdd = (pred x).toAdd :=
  rfl

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