fact_one_le_one_ennreal

Mathlib.Data.ENNReal.Basic

URI: https://scilib.ai/kg/mathlib#fact_one_le_one_ennreal

English

The fact that 1 ≤ 1 holds in ENNReal.

Русский

Факт: 1 ≤ 1 действительно в ENNReal.

LaTeX

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

Lean4

/-- `(1 : ℝ≥0∞) ≤ 1`, recorded as a `Fact` for use with `Lp` spaces. -/
instance _root_.fact_one_le_one_ennreal : Fact ((1 : ℝ≥0∞) ≤ 1) :=
  ⟨le_rfl⟩

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

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

Разделы

Аффилиация

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