Commit 2023-05-17 22:53 d0c30e10

View on Github →

feat: port Analysis.SpecialFunctions.Trigonometric.Inverse (#4037)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/SpecialFunctions/Trigonometric/Inverse.lean

added theorem Real.arccos_cos

added theorem Real.arccos_eq_arcsin

added theorem Real.arccos_eq_pi

added theorem Real.arccos_eq_pi_div_two

added theorem Real.arccos_eq_pi_div_two_sub_arcsin

added theorem Real.arccos_eq_zero

added theorem Real.arccos_inj

added theorem Real.arccos_injOn

added theorem Real.arccos_le_pi

added theorem Real.arccos_le_pi_div_four

added theorem Real.arccos_le_pi_div_two

added theorem Real.arccos_lt_pi_div_two

added theorem Real.arccos_neg

added theorem Real.arccos_neg_one

added theorem Real.arccos_nonneg

added theorem Real.arccos_of_le_neg_one

added theorem Real.arccos_of_one_le

added theorem Real.arccos_one

added theorem Real.arccos_pos

added theorem Real.arccos_zero

added theorem Real.arcsin_eq_arccos

added theorem Real.arcsin_eq_iff_eq_sin

added theorem Real.arcsin_eq_neg_pi_div_two

added theorem Real.arcsin_eq_of_sin_eq

added theorem Real.arcsin_eq_pi_div_two

added theorem Real.arcsin_eq_pi_div_two_sub_arccos

added theorem Real.arcsin_eq_zero_iff

added theorem Real.arcsin_inj

added theorem Real.arcsin_le_iff_le_sin'

added theorem Real.arcsin_le_iff_le_sin

added theorem Real.arcsin_le_neg_pi_div_two

added theorem Real.arcsin_le_pi_div_two

added theorem Real.arcsin_lt_iff_lt_sin'

added theorem Real.arcsin_lt_iff_lt_sin

added theorem Real.arcsin_lt_pi_div_two

added theorem Real.arcsin_lt_zero

added theorem Real.arcsin_mem_Icc

added theorem Real.arcsin_neg

added theorem Real.arcsin_neg_one

added theorem Real.arcsin_nonneg

added theorem Real.arcsin_nonpos

added theorem Real.arcsin_of_le_neg_one

added theorem Real.arcsin_of_one_le

added theorem Real.arcsin_one

added theorem Real.arcsin_pos

added theorem Real.arcsin_projIcc

added theorem Real.arcsin_sin'

added theorem Real.arcsin_sin

added theorem Real.arcsin_zero

added theorem Real.continuousAt_arcsin

added theorem Real.continuous_arccos

added theorem Real.continuous_arcsin

added theorem Real.cos_arccos

added theorem Real.cos_arcsin

added theorem Real.cos_arcsin_nonneg

added theorem Real.injOn_arcsin

added theorem Real.le_arcsin_iff_sin_le'

added theorem Real.le_arcsin_iff_sin_le

added theorem Real.lt_arcsin_iff_sin_lt'

added theorem Real.lt_arcsin_iff_sin_lt

added theorem Real.mapsTo_sin_Ioo

added theorem Real.monotone_arcsin

added theorem Real.neg_pi_div_two_eq_arcsin

added theorem Real.neg_pi_div_two_le_arcsin

added theorem Real.neg_pi_div_two_lt_arcsin

added theorem Real.pi_div_four_le_arcsin

added theorem Real.pi_div_two_eq_arcsin

added theorem Real.pi_div_two_le_arcsin

added theorem Real.range_arcsin

added def Real.sinLocalHomeomorph

added theorem Real.sin_arccos

added theorem Real.sin_arcsin'

added theorem Real.sin_arcsin

added theorem Real.strictAntiOn_arccos

added theorem Real.strictMonoOn_arcsin

added theorem Real.tan_arccos

added theorem Real.tan_arcsin

added theorem Real.zero_eq_arcsin_iff