canLift — Mathlib

English

There exists a CanLift from ENNReal to NNReal on finite values: ENNReal can be lifted to NNReal when the value is not ∞.

Русский

Существует CanLift из ENNReal в NNReal на конечных значениях: ENNReal можно поднять к NNReal, если значение не равно ∞.

LaTeX

$$$\text{CanLift }(\mathbb{R}_{\ge 0}^\infty \;\;\mathbb{R}_{\ge 0}, \, (\neq \infty)).$$$

Lean4

instance canLift : CanLift ℝ≥0∞ ℝ≥0 ofNNReal (· ≠ ∞) :=
  WithTop.canLift

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