two_le_pi

Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

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

English

2 ≤ π.

Русский

2 ≤ π.

LaTeX

$$$2 \le \pi$$$

Lean4

theorem two_le_pi : (2 : ℝ) ≤ π :=
  (div_le_div_iff_of_pos_right zero_lt_two).1 (by rw [div_self two_ne_zero]; exact one_le_pi_div_two)

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

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

Разделы

Аффилиация

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