bot_lt_coe_ennreal

Mathlib.Data.EReal.Basic

URI: https://scilib.ai/kg/mathlib#EReal.bot_lt_coe_ennreal

English

The bottom element of EReal is strictly below every embedded ENNReal.

Русский

Нижний элемент EReal строго меньше любого образа ENNReal.

LaTeX

$$$$ (\bot : EReal) < (x : EReal), \; x \in ENNReal. $$$$

Lean4

@[simp]
theorem bot_lt_coe_ennreal (x : ℝ≥0∞) : (⊥ : EReal) < x :=
  (bot_lt_coe 0).trans_le (coe_ennreal_nonneg _)

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

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

Разделы

Аффилиация

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