Commit 2022-10-21 17:19 b1a619c0
View on Github →refactor(analysis/special_functions/trigonometric/inverse): cos_arcsin
, sin_arccos
degenerate cases (#17026)
The definitions of arcsin
, arccos
and sqrt
in degenerate cases mean that the lemmas cos_arcsin
and sin_arccos
are actually true for all real arguments (including those outside the interval from -1 to 1), without needing any inequality hypotheses. Remove those inequality hypotheses from the lemmas, so simplifying use of those lemmas elsewhere.