English
a*b = top holds exactly in the following cases: a = bottom and b < 0; a < 0 and b = bottom; a = top and 0 < b; 0 < a and b = top.
Русский
Произведение a*b равно ⊤ ровно в следующих случаях: a = ⊥ и b < 0; a < 0 и b = ⊤; a = ⊤ и b > 0; a > 0 и b = ⊤.
LaTeX
$$$a \cdot b = \top \iff (a = \bot \land b < 0) \lor (a < 0 \land b = \bot) \lor (a = \top \land 0 < b) \lor (0 < a \land b = \top)$$$
Lean4
theorem mul_eq_top (a b : EReal) : a * b = ⊤ ↔ (a = ⊥ ∧ b < 0) ∨ (a < 0 ∧ b = ⊥) ∨ (a = ⊤ ∧ 0 < b) ∨ (0 < a ∧ b = ⊤) :=
by
induction a, b using EReal.induction₂_symm with
| symm h => grind [EReal.mul_comm]
| top_top => simp
| top_pos _ hx => simp [EReal.top_mul_coe_of_pos hx, hx]
| top_zero => simp
| top_neg _ hx => simp [hx.le, EReal.top_mul_coe_of_neg hx]
| top_bot => simp
| pos_bot _ hx => simp [hx.le, EReal.coe_mul_bot_of_pos hx]
| coe_coe x y =>
simpa only [EReal.coe_ne_bot, EReal.coe_neg', false_and, and_false, EReal.coe_ne_top, EReal.coe_pos, or_self,
iff_false, EReal.coe_mul] using EReal.coe_ne_top _
| zero_bot => simp
| neg_bot _ hx => simp [hx, EReal.coe_mul_bot_of_neg hx]
| bot_bot => simp
