exp_one_gt_d9

Mathlib.Analysis.Complex.ExponentialBounds

URI: https://scilib.ai/kg/mathlib#Real.exp_one_gt_d9

English

exp(1) > 2.7182818283.

Русский

Exp(1) больше, чем 2.7182818283.

LaTeX

$$$\exp(1) > 2.7182818283$$$

Lean4

theorem exp_one_gt_d9 : 2.7182818283 < exp 1 :=
  lt_of_lt_of_le (by norm_num) (sub_le_comm.1 (abs_sub_le_iff.1 exp_one_near_10).2)

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

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

Разделы

Аффилиация

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