preimage_coe_nnreal_real — Mathlib

English

If a set s is OrdConnected in Real, then its preimage under the embedding into NNReal is OrdConnected.

Русский

Если множество s упорядоченно связно в ℝ, то его предобраз под встраиванием в ℝ≥0 также упорядоченно связано.

LaTeX

$$$ (h : s.OrdConnected) \Rightarrow ((↑)^{-1} s : Set \mathbb{R}_{\ge 0}).OrdConnected $$$

Lean4

theorem preimage_coe_nnreal_real (h : s.OrdConnected) : ((↑) ⁻¹' s : Set ℝ≥0).OrdConnected :=
  h.preimage_mono NNReal.coe_mono

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