mulRightReflectLT_of_mulRightMono

English

If right translations are monotone, then right translations reflect the strict order: μ(a,c) < μ(b,c) implies a < b.

Русский

Если правые переносы монотонны, то правые переносы отражают строгий порядок: μ(a,c) < μ(b,c) ⇒ a < b.

LaTeX

$$$\forall a,b,c\in N\; r(μ(a,c), μ(b,c)) \Rightarrow r(a,b)$$$

Lean4

@[to_additive]
theorem mulRightReflectLT_of_mulRightMono [Mul N] [LinearOrder N] [MulRightMono N] : MulRightReflectLT N :=
  inferInstance

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