Sum_of_Arcsine_and_Arccosine
Provedarccosine-functionarcsine-functionproofwiki
Let be a real number such that . Then where and denote arcsine and arccosine respectively.
Preamble
import Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Formal statement
theorem Sum_of_Arcsine_and_Arccosine (x : ℝ) (hx : x ∈ Set.Icc (-1 : ℝ) 1) : Real.arcsin x + Real.arccos x = Real.pi / 2 := by sorry
Source