English
a*b = bottom holds exactly in the following cases: a = bottom and 0 < b; 0 < a and b = bottom; a = top and b < 0; a < 0 and b = top.
Русский
Произведение a*b равно ⊥ ровно в следующих случаях: a = ⊥ и 0 < b; 0 < a и b = ⊥; a = ⊤ и b < 0; a < 0 и b = ⊤.
LaTeX
$$a * b = \bot \iff (a = \bot \land 0 < b) \lor (0 < a \land b = \bot) \lor (a = \top \land b < 0) \lor (a < 0 \land b = \top)$$
Lean4
theorem mul_eq_bot (a b : EReal) : a * b = ⊥ ↔ (a = ⊥ ∧ 0 < b) ∨ (0 < a ∧ b = ⊥) ∨ (a = ⊤ ∧ b < 0) ∨ (a < 0 ∧ b = ⊤) :=
by
rw [← neg_eq_top_iff, ← EReal.neg_mul, mul_eq_top, neg_eq_bot_iff, neg_eq_top_iff, neg_lt_comm, lt_neg_comm, neg_zero]
tauto
