English
For extended reals a,b, the statement 0 < a*b is equivalent to certain sign conditions, as in the previous lemma, but expressed in a more general framework. In particular, the result mirrors the standard sign rule for multiplication.
Русский
Для расширенных вещественных чисел a,b верно: 0 < a*b эквивалентно определённым знакам a и b, аналогично обычному правилу знаков при умножении.
LaTeX
$$$0 < a b \iff (0 < a \land 0 < b) \lor (a < 0 \land b < 0)$$$
Lean4
theorem mul_pos_iff {a b : EReal} : 0 < a * b ↔ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0 := by
induction a, b using EReal.induction₂_symm with
| symm h => simp [EReal.mul_comm, h, and_comm]
| top_top => simp
| top_pos _ hx => simp [EReal.top_mul_coe_of_pos hx, hx]
| top_zero => simp
| top_neg _ hx => simp [hx, EReal.top_mul_coe_of_neg hx, le_of_lt]
| top_bot => simp
| pos_bot _ hx => simp [hx, EReal.coe_mul_bot_of_pos hx, le_of_lt]
| coe_coe x y => simp [← coe_mul, _root_.mul_pos_iff]
| zero_bot => simp
| neg_bot _ hx => simp [hx, EReal.coe_mul_bot_of_neg hx]
| bot_bot => simp
