x : ℝ
hx : x ∈ interior (Icc (-(π / 2)) (π / 2))
⊢ (deriv^[2]) cos x < 0
⊢ StrictConcaveOn ℝ (Icc (-(π / 2)) (π / 2)) cos
apply strictConcaveOn_of_deriv2_neg (convex_Icc _ _) continuousOn_cos fun x hx => ?_
x : ℝ
hx : x ∈ Ioo (-(π / 2)) (π / 2)
⊢ (deriv^[2]) cos x < 0
x : ℝ
hx : x ∈ interior (Icc (-(π / 2)) (π / 2))
⊢ (deriv^[2]) cos x < 0
rw [interior_Icc] at hx
no goals
x : ℝ
hx : x ∈ Ioo (-(π / 2)) (π / 2)
⊢ (deriv^[2]) cos x < 0
simp [cos_pos_of_mem_Ioo hx]