fact_one_le_two_ennreal

Mathlib.Data.ENNReal.Basic

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

← MathLib Explorer

English

The fact that 1 ≤ 2 holds in ENNReal.

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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