lt_or_lt_of_mul_lt_mul — Mathlib

English

Let α be a linearly ordered set with Mul α, MulLeftMono α, and MulRightMono α. If a1 < a2 and b1 < b2 then a1·b1 < a2·b2; more generally, if a1·b1 < a2·b2, then a1 < a2 or b1 < b2.

Русский

Пусть α упорядочено линейно и имеется умножение, монотонность слева и справа. Тогда если a1 < a2 и b1 < b2, то a1·b1 < a2·b2; более общо: a1·b1 < a2·b2 влечет a1 < a2 или b1 < b2.

LaTeX

$$$ a_1 b_1 < a_2 b_2 \quad\Rightarrow\quad a_1 < a_2 \; \lor \; b_1 < b_2 $$$

Lean4

@[to_additive]
theorem lt_or_lt_of_mul_lt_mul [MulLeftMono α] [MulRightMono α] {a₁ a₂ b₁ b₂ : α} :
    a₁ * b₁ < a₂ * b₂ → a₁ < a₂ ∨ b₁ < b₂ := by
  contrapose!
  exact fun h => mul_le_mul' h.1 h.2

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