toReal_pos

Mathlib.Data.ENNReal.Real

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

← MathLib Explorer

English

If a ≠ 0 and a ≠ ∞, then 0 < a.toReal.

Русский

Если a ≠ 0 и a ≠ ∞, то 0 < a.toReal.

LaTeX

$$$$ \\forall a \\in \\mathbb{R}_{\\ge 0}^{\\infty},\\; a \\neq 0 \\land a \\neq \\infty \\Rightarrow 0 < a^{\\mathrm{toReal}}. $$$$

Lean4

theorem toReal_pos {a : ℝ≥0∞} (ha₀ : a ≠ 0) (ha_top : a ≠ ∞) : 0 < a.toReal :=
  toReal_pos_iff.mpr ⟨bot_lt_iff_ne_bot.mpr ha₀, lt_top_iff_ne_top.mpr ha_top⟩

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

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

Разделы

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

Аффилиация

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