English
The product a·b is finite exactly when either both factors are finite or one factor is zero.
Русский
Произведение a·b конечно тогда, когда либо оба коэффициента конечны, либо один из них равен нулю.
LaTeX
$$$a \cdot b < \infty \iff (a < \infty \land b < \infty) \lor a = 0 \lor b = 0$$$
Lean4
theorem mul_lt_top_iff {a b : ℝ≥0∞} : a * b < ∞ ↔ a < ∞ ∧ b < ∞ ∨ a = 0 ∨ b = 0 :=
by
constructor
· intro h
rw [← or_assoc, or_iff_not_imp_right, or_iff_not_imp_right]
intro hb ha
exact ⟨lt_top_of_mul_ne_top_left h.ne hb, lt_top_of_mul_ne_top_right h.ne ha⟩
· rintro (⟨ha, hb⟩ | rfl | rfl) <;> [exact mul_lt_top ha hb; simp; simp]