exp_lt_top_iff

Mathlib.Analysis.SpecialFunctions.Log.ERealExp

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

English

For all a ∈ EReal, exp a < ∞ iff a < ∞.

Русский

Для каждого a ∈ EReal, exp a < ∞ тогда и только тогда, когда a < ∞.

LaTeX

$$$\forall a:\, \mathrm{EReal},\ exp(a) < \top \iff a < \top$$$

Lean4

@[simp]
theorem exp_lt_top_iff {a : EReal} : exp a < ⊤ ↔ a < ⊤ :=
  exp_top ▸ @exp_lt_exp_iff a ⊤

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

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

Разделы

Аффилиация

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