sqrt_two_lt_three_halves

Mathlib.Data.Real.Sqrt

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

← MathLib Explorer

English

√2 < 3/2.

Русский

√2 меньше чем 3/2.

LaTeX

$$$\sqrt{2} < \tfrac{3}{2}$$$

Lean4

theorem sqrt_two_lt_three_halves : √2 < 3 / 2 :=
  by
  suffices 2 * √2 < 3 by linarith
  rw [← sq_lt_sq₀ (by positivity) (by positivity), mul_pow, Real.sq_sqrt (by positivity)]
  norm_num

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

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

Разделы

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

Аффилиация

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