English
For extended real numbers a, b, 0 < a*b holds exactly when either both a and b are positive or both are negative.
Русский
Для расширенных вещественных чисел a, b верно: 0 < a·b тогда и только тогда, когда либо обе величины положительны, либо обе отрицательны.
LaTeX
$$$0 < a b \iff (0 < a \land 0 < b) \lor (a < 0 \land b < 0)$$$
Lean4
instance : NoZeroDivisors EReal where
eq_zero_or_eq_zero_of_mul_eq_zero := by
intro a b h
contrapose! h
cases a <;> cases b <;>
try { · simp_all [← EReal.coe_mul]
}
· rcases lt_or_gt_of_ne h.2 with (h | h) <;> simp [EReal.bot_mul_of_neg, EReal.bot_mul_of_pos, h]
· rcases lt_or_gt_of_ne h.1 with (h | h) <;> simp [EReal.mul_bot_of_pos, EReal.mul_bot_of_neg, h]
· rcases lt_or_gt_of_ne h.1 with (h | h) <;> simp [EReal.mul_top_of_neg, EReal.mul_top_of_pos, h]
· rcases lt_or_gt_of_ne h.2 with (h | h) <;> simp [EReal.top_mul_of_pos, EReal.top_mul_of_neg, h]
