preimage_coe_nnreal_ennreal — Mathlib

English

If u ⊆ ENNReal is ordered-connected, then its preimage under the natural embedding from NNReal is ordered-connected.

Русский

Если u ⊆ ENNReal имеет свойство упорядоченной связности, то её предобраз через естественное вложение NNReal в ENNReal тоже упорядоченно-связный.

LaTeX

$$$$\\text{If } u.OrdConnected, \\ ((↑)^{-1}' u).OrdConnected.$$$$

Lean4

theorem preimage_coe_nnreal_ennreal (h : u.OrdConnected) : ((↑) ⁻¹' u : Set ℝ≥0).OrdConnected :=
  h.preimage_mono ENNReal.coe_mono

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