instCanLiftENNRealToERealLeOfNat

Mathlib.Data.EReal.Basic

URI: https://scilib.ai/kg/mathlib#EReal.instCanLiftENNRealToERealLeOfNat

English

There exists an order-preserving lifting of ENNReal to EReal along the embedding.

Русский

Существует построение (подъём) ENNReal в EReal, сохраняющее порядок.

LaTeX

$$$$ \exists L: ENNReal \to EReal,\ \text{Monotone}(L). $$$$

Lean4

instance : CanLift EReal ℝ≥0∞ (↑) (0 ≤ ·) :=
  ⟨range_coe_ennreal.ge⟩

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

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

Разделы

Аффилиация

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