le_or_lt_of_mul_le_mul — Mathlib

English

Under MulLeftMono α and MulRightStrictMono α, for all a1, a2, b1, b2 ∈ α, a1 b1 ≤ a2 b2 implies a1 ≤ a2 or b1 < b2.

Русский

При MulLeftMono α и MulRightStrictMono α, для любых a1, a2, 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 < b_2 $$$

Lean4

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

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