mulLeftReflectLT_of_mulLeftMono — Mathlib

English

If left translations are monotone, then left 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 mulLeftReflectLT_of_mulLeftMono [Mul N] [LinearOrder N] [MulLeftMono N] : MulLeftReflectLT N :=
  inferInstance

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