English
a*b ≠ top iff a ≠ bottom or 0 ≤ b, and 0 ≤ a or b ≠ bottom, and a ≠ top or b ≤ 0, and a ≤ 0 or b ≠ top.
Русский
Произведение a*b не равно ⊤ тогда и только тогда, когда выполняются соответствующие четыре условия.
LaTeX
$$a * b ≠ \top \iff (a ≠ \bot \lor 0 \le b) \land (0 \le a \lor b ≠ \bot) \land (a \neq \top \lor b \le 0) \land (a \le 0 \lor b \neq \top)$$
Lean4
theorem mul_ne_top (a b : EReal) : a * b ≠ ⊤ ↔ (a ≠ ⊥ ∨ 0 ≤ b) ∧ (0 ≤ a ∨ b ≠ ⊥) ∧ (a ≠ ⊤ ∨ b ≤ 0) ∧ (a ≤ 0 ∨ b ≠ ⊤) :=
by
rw [ne_eq, mul_eq_top]
-- push the negation while keeping the disjunctions, that is converting `¬(p ∧ q)` into `¬p ∨ ¬q`
-- rather than `p → ¬q`, since we already have disjunctions in the rhs
set_option push_neg.use_distrib true in push_neg
rfl
