mul_lt_mul — Mathlib

English

If left multiplication is strictly monotone and right multiplication is monotone, then for all a, b, c, d in α, a < b and c < d imply a · c < b · d.

Русский

Если левая операция умножения строго монотонна, а правая монотонна, то для любых a, b, c, d в α верно: a < b и c < d ⇒ a·c < b·d.

LaTeX

$$$$ \\forall a,b,c,d \\in \\alpha,\; a < b \\to c < d \\to a \\cdot c < b \\cdot d $$$$

Lean4

/-- Only assumes left strict covariance. -/
@[to_additive /-- Only assumes left strict covariance -/
    ]
theorem mul_lt_mul [MulLeftStrictMono α] [MulRightMono α] {a b c d : α} (h₁ : a < b) (h₂ : c < d) : a * c < b * d :=
  mul_lt_mul_of_le_of_lt h₁.le h₂

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