toENNReal_lt

Mathlib.Data.Real.ENatENNReal

URI: https://scilib.ai/kg/mathlib#ENat.toENNReal_lt

English

The embedding preserves strict order: m < n in ENat iff their images satisfy (m:ℝ≥0∞) < (n:ℝ≥0∞).

Русский

Встраивание сохраняет строгий порядок: m < n эквивалентно образам (m) < (n).

LaTeX

$$$(m : \\mathbb{R}_{\\ge 0,\\infty}) < n \\iff m < n.$$$

Lean4

@[simp, norm_cast]
theorem toENNReal_lt : (m : ℝ≥0∞) < n ↔ m < n :=
  toENNRealOrderEmbedding.lt_iff_lt

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

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

Разделы

Аффилиация

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