exp_lt_one_iff

Mathlib.Analysis.SpecialFunctions.Log.ERealExp

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

English

exp a < 1 iff a < 0.

Русский

exp a < 1 тогда и только тогда, когда a < 0.

LaTeX

$$$\exp(a) < 1 \iff a < 0$$$

Lean4

@[simp]
theorem exp_lt_one_iff {a : EReal} : exp a < 1 ↔ a < 0 :=
  exp_zero ▸ @exp_lt_exp_iff a 0

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

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

Разделы

Аффилиация

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