one_lt_two

Mathlib.Data.ENNReal.Basic

URI: https://scilib.ai/kg/mathlib#ENNReal.one_lt_two

English

In ENNReal, 1 < 2.

Русский

В ENNReal 1 < 2.

LaTeX

$$$ (1 : \mathbb{R}_{\ge 0}^{\infty}) < 2 $$$

Lean4

theorem one_lt_two : (1 : ℝ≥0∞) < 2 :=
  Nat.one_lt_ofNat

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

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

Разделы

Аффилиация

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