English
The subset of ENNReal not equal to ∞ is in bijection with NNReal via x ↦ toNNReal x and its inverse x ↦ ⟨x, coe_ne_top⟩.
Русский
Подмножество ENNReal, состоящее из значений, не равных ∞, образует биекцию с NNReal через x ↦ toNNReal x и обратное x ↦ ⟨x, coe_ne_top⟩.
LaTeX
$$$ {a \in \mathbb{R}_{\ge 0}^{\infty} \mid a \neq \infty} \simeq \mathbb{R}_{\ge 0}, \; toFun(a) = toNNReal(a), \; invFun(x) = \langle x, coe\_ne\_top \rangle $$$
Lean4
/-- The set of numbers in `ℝ≥0∞` that are not equal to `∞` is equivalent to `ℝ≥0`. -/
def neTopEquivNNReal : {a | a ≠ ∞} ≃ ℝ≥0 where
toFun x := ENNReal.toNNReal x
invFun x := ⟨x, coe_ne_top⟩
left_inv := fun x => Subtype.eq <| coe_toNNReal x.2
right_inv := toNNReal_coe
