instPredOrderMultiplicative — Mathlib

English

If X is a preorder with a predecessor order, then the multiplicative structure on X inherits the same predecessor order: PredOrder (Multiplicative X).

Русский

Если X — предorder с предшествующим порядком, то у множителя X сохраняется тот же порядок: PredOrder (Multiplicative X).

LaTeX

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

Lean4

instance [Preorder X] [h : PredOrder X] : PredOrder (Multiplicative X) :=
  h

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