toNNReal_eq_toNNReal_iff' — Mathlib

English

For x, y in ENNReal with x ≠ ∞ and y ≠ ∞, x.toNNReal = y.toNNReal iff x = y.

Русский

Для x, y в ENNReal при условии x ≠ ∞ и y ≠ ∞, x.toNNReal = y.toNNReal тогда и только тогда, когда x = y.

LaTeX

$$$ x \neq \infty \land y \neq \infty \Rightarrow x.toNNReal = y.toNNReal \iff x = y $$$

Lean4

theorem toNNReal_eq_toNNReal_iff' {x y : ℝ≥0∞} (hx : x ≠ ⊤) (hy : y ≠ ⊤) : x.toNNReal = y.toNNReal ↔ x = y := by
  simp only [ENNReal.toNNReal_eq_toNNReal_iff x y, hx, hy, and_false, false_and, or_false]

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