fact_one_le_top_ennreal

Mathlib.Data.ENNReal.Basic

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

English

The fact that 1 ≤ ∞ holds in ENNReal.

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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