one_le_exp_iff

Mathlib.Analysis.SpecialFunctions.Log.ERealExp

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

English

1 ≤ exp a iff 0 ≤ a.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem one_le_exp_iff {a : EReal} : 1 ≤ exp a ↔ 0 ≤ a :=
  exp_zero ▸ @exp_le_exp_iff 0 a

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

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

Разделы

Аффилиация

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