exp_le_exp_iff

Mathlib.Analysis.SpecialFunctions.Log.ERealExp

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

English

exp a ≤ exp b iff a ≤ b.

Русский

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

LaTeX

$$$\exp(a) \leq \exp(b) \iff a \leq b$$$

Lean4

@[simp]
theorem exp_le_exp_iff {a b : EReal} : exp a ≤ exp b ↔ a ≤ b :=
  exp_strictMono.le_iff_le

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

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

Разделы

Аффилиация

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