preimage_real_toNNReal

Mathlib.Data.NNReal.Defs

URI: https://scilib.ai/kg/mathlib#Set.OrdConnected.preimage_real_toNNReal

English

If t is OrdConnected, then the preimage under Real.toNNReal is OrdConnected.

Русский

Если t упорядоченно связано в ℝ≥0, то предобраз Real.toNNReal t упорядоченно связан.

LaTeX

$$$ (h : t.OrdConnected) : (Real.toNNReal ^{-1} t).OrdConnected $$$

Lean4

theorem preimage_real_toNNReal (h : t.OrdConnected) : (Real.toNNReal ⁻¹' t).OrdConnected :=
  h.preimage_mono Real.toNNReal_monotone

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru