preimage_ennreal_ofReal — Mathlib

English

If u ⊆ ENNReal is ordered-connected, then the preimage of u under ENNReal.ofReal is ordered-connected.

Русский

Если u ⊆ ENNReal упорядоченно-связно, то предобраз u через ENNReal.ofReal также упорядоченно-связен.

LaTeX

$$$$ (\\mathrm{ofReal})^{-1}' u.OrdConnected $$$$

Lean4

theorem preimage_ennreal_ofReal (h : u.OrdConnected) : (ENNReal.ofReal ⁻¹' u).OrdConnected :=
  h.preimage_coe_nnreal_ennreal.preimage_real_toNNReal

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