English
If s is OrdConnected in Real, then its image under toNNReal is OrdConnected in NNReal.
Русский
Если s упорядоченно связано в ℝ, то его образ под Real.toNNReal в ℝ≥0 является упорядочно связанным.
LaTeX
$$$ (h : s.OrdConnected) : (Real.toNNReal '' s).OrdConnected $$$
Lean4
theorem image_real_toNNReal (h : s.OrdConnected) : (Real.toNNReal '' s).OrdConnected :=
by
refine ⟨forall_mem_image.2 fun x hx => forall_mem_image.2 fun y hy z hz => ?_⟩
rcases le_total y 0 with hy₀ | hy₀
· rw [mem_Icc, Real.toNNReal_of_nonpos hy₀, nonpos_iff_eq_zero] at hz
exact ⟨y, hy, (toNNReal_of_nonpos hy₀).trans hz.2.symm⟩
· lift y to ℝ≥0 using hy₀
rw [toNNReal_coe] at hz
exact ⟨z, h.out hx hy ⟨toNNReal_le_iff_le_coe.1 hz.1, hz.2⟩, toNNReal_coe⟩
