toNNReal_eq_toNNReal_iff — Mathlib

English

For x, y in ENNReal, x.toNNReal = y.toNNReal iff x = y or x = 0 ∧ y = ∞ or x = ∞ ∧ y = 0.

Русский

Для x, y в ENNReal выполняется: x.toNNReal = y.toNNReal тогда и только тогда, когда x = y, или x = 0 и y = ∞, или x = ∞ и y = 0.

LaTeX

$$$ x.toNNReal = y.toNNReal \iff x = y \lor x = 0 \land y = \top \lor x = \top \land y = 0 $$$

Lean4

theorem toNNReal_eq_toNNReal_iff (x y : ℝ≥0∞) : x.toNNReal = y.toNNReal ↔ x = y ∨ x = 0 ∧ y = ⊤ ∨ x = ⊤ ∧ y = 0 :=
  WithTop.untopD_eq_untopD_iff

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