sin_sq_le_sq

Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds

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

English

For all x, sin^2 x ≤ x^2.

Русский

Для всех x выполнено sin^2 x ≤ x^2.

LaTeX

$$$$ \\sin^2 x \\le x^2. $$$$

Lean4

theorem sin_sq_le_sq : sin x ^ 2 ≤ x ^ 2 :=
  by
  rcases eq_or_ne x 0 with rfl | hx
  case inl => simp
  case inr => exact (sin_sq_lt_sq hx).le

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

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

Разделы

Аффилиация

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