English
There exists an order isomorphism between the extended nonnegative real numbers and the unit interval.
Русский
Существует упорядоченная изоморфия между расширенными неотрицательными числами и монадным интервалом единицы.
LaTeX
$$$$ \mathbb{R}_{\ge 0}^{\infty} \cong_o Iic(1). $$$$
Lean4
/-- The birational order isomorphism between `ℝ≥0∞` and the unit interval `Set.Iic (1 : ℝ≥0∞)`. -/
@[simps! apply_coe]
def orderIsoIicOneBirational : ℝ≥0∞ ≃o Iic (1 : ℝ≥0∞) :=
by
refine
StrictMono.orderIsoOfRightInverse (fun x => ⟨(x⁻¹ + 1)⁻¹, ENNReal.inv_le_one.2 <| le_add_self⟩) (fun x y hxy => ?_)
(fun x => (x.1⁻¹ - 1)⁻¹) fun x => Subtype.ext ?_
· simpa only [Subtype.mk_lt_mk, ENNReal.inv_lt_inv, ENNReal.add_lt_add_iff_right one_ne_top]
· have : (1 : ℝ≥0∞) ≤ x.1⁻¹ := ENNReal.one_le_inv.2 x.2
simp only [inv_inv, tsub_add_cancel_of_le this]
