orderIsoUnitIntervalBirational_apply_coe

English

For x ∈ ENNReal, (orderIsoUnitIntervalBirational x : ℝ) = (x^{-1} + 1)^{-1}.toReal.

Русский

Для x ∈ ENNReal выполняется (orderIsoUnitIntervalBirational x).toReal = (x^{-1} + 1)^{-1}.toReal.

LaTeX

$$$$ (orderIsoUnitIntervalBirational\, x : \mathbb{R}) = (x^{-1} + 1)^{-1}.toReal. $$$$

Lean4

@[simp]
theorem orderIsoUnitIntervalBirational_apply_coe (x : ℝ≥0∞) :
    (orderIsoUnitIntervalBirational x : ℝ) = (x⁻¹ + 1)⁻¹.toReal :=
  rfl

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