exists_cos_eq_zero

Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic

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

← MathLib Explorer

English

There exists a point t in [1,2] such that cos t = 0.

Русский

Существует t ∈ [1,2] такое, что cos t = 0.

LaTeX

$$0 ∈ cos '' Icc (1 : ℝ) 2$$

Lean4

theorem exists_cos_eq_zero : 0 ∈ cos '' Icc (1 : ℝ) 2 :=
  intermediate_value_Icc' (by simp) continuousOn_cos ⟨le_of_lt cos_two_neg, le_of_lt cos_one_pos⟩

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

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

Разделы

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

Аффилиация

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