English
Let α be a linear order with Mul α, with left/right monotone and strict-monotone properties. For a1 ≤ a2 and b1 ≤ b2, a1 b1 < a2 b2 holds iff a1 < a2 or b1 < b2.
Русский
Пусть α упорядочено линейно, есть умножение слева и справа с монотонностями. При a1 ≤ a2 и b1 ≤ b2 выполняется a1 b1 < a2 b2 тогда и только тогда, когда a1 < a2 или b1 < b2.
LaTeX
$$$ \ big Iff \ (a_1 b_1 < a_2 b_2) \iff (a_1 < a_2 \lor b_1 < b_2) $$$
Lean4
@[to_additive]
theorem mul_lt_mul_iff_of_le_of_le [MulLeftMono α] [MulRightMono α] [MulLeftStrictMono α] [MulRightStrictMono α]
{a₁ a₂ b₁ b₂ : α} (ha : a₁ ≤ a₂) (hb : b₁ ≤ b₂) : a₁ * b₁ < a₂ * b₂ ↔ a₁ < a₂ ∨ b₁ < b₂ :=
by
refine ⟨lt_or_lt_of_mul_lt_mul, fun h => ?_⟩
rcases h with ha' | hb'
· exact mul_lt_mul_of_lt_of_le ha' hb
· exact mul_lt_mul_of_le_of_lt ha hb'
