log_two_lt_d9

Mathlib.Analysis.Complex.ExponentialBounds

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

English

log 2 < 0.6931471808.

Русский

log 2 < 0.6931471808

LaTeX

$$$\log 2 < 0.6931471808$$$

Lean4

theorem log_two_lt_d9 : log 2 < 0.6931471808 :=
  lt_of_le_of_lt (sub_le_iff_le_add.1 (abs_sub_le_iff.1 log_two_near_10).1) (by norm_num)

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

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

Разделы

Аффилиация

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