image_coe_nnreal_real — Mathlib

English

If t is OrdConnected, then its image under the real-to-NNReal embedding is OrdConnected.

Русский

Если t упорядоченно связано в ℝ, то его образ под отображением Real.toNNReal/tом NNReal упорядоченно связано.

LaTeX

$$$ (h : t.OrdConnected) : (\mathrm{Real.toNNReal} '' t).OrdConnected $$$

Lean4

theorem image_coe_nnreal_real (h : t.OrdConnected) : ((↑) '' t : Set ℝ).OrdConnected :=
  ⟨forall_mem_image.2 fun x hx => forall_mem_image.2 fun _y hy z hz => ⟨⟨z, x.2.trans hz.1⟩, h.out hx hy hz, rfl⟩⟩
    -- TODO: does it generalize to a `GaloisInsertion`?

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