mul_lt_top_iff — Mathlib

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]

Похожие утверждения