one_lt_exp_iff

Mathlib.Analysis.SpecialFunctions.Log.ERealExp

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

English

1 < exp a iff 0 < a.

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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