pi_gt_d4

Mathlib.Analysis.Real.Pi.Bounds

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

← MathLib Explorer

English

π is greater than 3.1415.

Русский

π больше 3.1415.

LaTeX

$$$3.1415 < \\pi$$$

Lean4

theorem pi_gt_d4 : 3.1415 < π := by
  -- bound[31415*^-4, Iters -> 6, Rounding -> 1.1, Precision -> 10]
  pi_lower_bound [1970 / 1393, 3010 / 1629, 11689 / 5959, 10127 / 5088, 33997 / 17019, 23235 / 11621]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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