mul_eq_top — Mathlib

English

In ENNReal, the product a·b equals ∞ exactly when one factor is ∞ and the other is nonzero (including the case both are ∞).

Русский

В ENNReal произведение a·b равно ∞ тогда, когда хотя бы один фактор равен ∞ и другой не равен нулю (включая случай, когда оба равны ∞).

LaTeX

$$$a \cdot b = \infty \;\iff\; (a \neq 0 \land b = \infty) \lor (a = \infty \land b \neq 0)$$$

Lean4

theorem mul_eq_top : a * b = ∞ ↔ a ≠ 0 ∧ b = ∞ ∨ a = ∞ ∧ b ≠ 0 :=
  WithTop.mul_eq_top_iff

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