inverse): `arccos_pos`, `arccos_lt_pi_div_two` (#17111)

Commit

3 years ago

feat(analysis/special_functions/trigonometric/inverse): `arccos_pos`, `arccos_lt_pi_div_two` (#17111) Add two more lemmas about inequalities for `arccos`.

Author

jsm28

Parents

0437938e

mathlib 44682c2d - feat(analysis/special_functions/trigonometric/inverse): `arccos_pos`, `arccos_lt_pi_div_two` (#17111)

mathlib
44682c2d - feat(analysis/special_functions/trigonometric/inverse): `arccos_pos`, `arccos_lt_pi_div_two` (#17111)