zero_lt_exp_iff

Mathlib.Analysis.SpecialFunctions.Log.ERealExp

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

English

0 < exp a iff ⊥ < a.

Русский

0 < exp a эквивалентно ⊥ < a.

LaTeX

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

Lean4

@[simp]
theorem zero_lt_exp_iff {a : EReal} : 0 < exp a ↔ ⊥ < a :=
  exp_bot ▸ @exp_lt_exp_iff ⊥ a

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

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

Разделы

Аффилиация

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