pi_le_four

Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

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

← MathLib Explorer

English

π is bounded above by 4.

Русский

π не превосходит 4.

LaTeX

$$$\pi \le 4$$$

Lean4

theorem pi_le_four : π ≤ 4 :=
  (div_le_div_iff_of_pos_right zero_lt_two).1
    (calc
      π / 2 ≤ 2 := pi_div_two_le_two
      _ = 4 / 2 := by norm_num)

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

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

Разделы

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

Аффилиация

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