le_or_le_of_mul_le_mul — Mathlib

English

Let α be a linearly ordered set with Mul α, MulLeftStrictMono α and MulRightStrictMono α. If a1 b1 ≤ a2 b2, then a1 ≤ a2 or b1 ≤ b2.

Русский

Пусть α упорядочено линейно с умножением и строгими монотонностями слева и справа. Если a1 b1 ≤ a2 b2, тогда a1 ≤ a2 или b1 ≤ b2.

LaTeX

$$$ a_1 b_1 \le a_2 b_2 \Rightarrow a_1 \le a_2 \; \lor \; b_1 \le b_2 $$$

Lean4

@[to_additive]
theorem le_or_le_of_mul_le_mul [MulLeftStrictMono α] [MulRightStrictMono α] {a₁ a₂ b₁ b₂ : α} :
    a₁ * b₁ ≤ a₂ * b₂ → a₁ ≤ a₂ ∨ b₁ ≤ b₂ := by
  contrapose!
  exact fun h => mul_lt_mul_of_lt_of_lt h.1 h.2

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