goldenRatio_lt_two

Mathlib.Data.Real.GoldenRatio

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

English

φ < 2

Русский

φ < 2

LaTeX

$$$ \phi < 2 $$$

Lean4

theorem goldenRatio_lt_two : φ < 2 := by
  calc
    (1 + √5) / 2 < (1 + 3) / 2 := by gcongr; rw [sqrt_lt'] <;> norm_num
    _ = 2 := by norm_num

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

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

Разделы

Аффилиация

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