image_coe_nnreal_ennreal — Mathlib

English

If t ⊆ NNReal is ordered-connected, then the image ENNReal.ofNNReal(t) ⊆ ENNReal is ordered-connected.

Русский

Если t ⊆ NNReal упорядочно-связно, то образ ENNReal.ofNNReal(t) в ENNReal также упорядочно-связен.

LaTeX

$$$$\\text{If } t.OrdConnected, \\ (\\mathrm{ENNReal}.ofNNReal '' t).OrdConnected.$$$$

Lean4

theorem image_coe_nnreal_ennreal (h : t.OrdConnected) : ((↑) '' t : Set ℝ≥0∞).OrdConnected :=
  by
  refine ⟨forall_mem_image.2 fun x hx => forall_mem_image.2 fun y hy z hz => ?_⟩
  rcases ENNReal.le_coe_iff.1 hz.2 with ⟨z, rfl, -⟩
  exact mem_image_of_mem _ (h.out hx hy ⟨ENNReal.coe_le_coe.1 hz.1, ENNReal.coe_le_coe.1 hz.2⟩)

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