lt_or_le_of_mul_le_mul — Mathlib

English

Let α be a linearly ordered set with Mul α, MulLeftMono α, and MulRightMono α. If a1 b1 < a2 b2, then a1 < a2 or b1 < b2 (in the semilattice sense).

Русский

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

LaTeX

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

Lean4

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

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