Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-18 01:44 b1218f8b

View on Github →

chore(analysis/special_functions/trigonometric): review, golf (#5392)

Estimated changes

Modified src/analysis/special_functions/trigonometric.lean

added theorem real.bij_on_cos

added theorem real.bij_on_sin

modified theorem real.cos_eq_one_iff_of_lt_of_lt

deleted theorem real.cos_inj_of_nonneg_of_le_pi

added theorem real.cos_mem_Icc

modified theorem real.cos_nonneg_of_mem_Icc

modified theorem real.cos_nonpos_of_pi_div_two_le_of_le

modified theorem real.cos_pos_of_mem_Ioo

deleted theorem real.exists_cos_eq

deleted theorem real.exists_sin_eq

added theorem real.inj_on_cos

added theorem real.inj_on_sin

added theorem real.maps_to_cos

added theorem real.maps_to_sin

modified theorem real.range_cos

modified theorem real.range_sin

deleted theorem real.sin_inj_of_le_of_le_pi_div_two

deleted theorem real.sin_lt_sin_of_le_of_le_pi_div_two

added theorem real.sin_lt_sin_of_lt_of_le_pi_div_two

added theorem real.sin_mem_Icc

added theorem real.sin_nonneg_of_mem_Icc

added theorem real.sin_pos_of_mem_Ioo

added theorem real.strict_mono_decr_on_cos

added theorem real.strict_mono_incr_on_sin

added theorem real.surj_on_cos

added theorem real.surj_on_sin

Modified src/geometry/euclidean/triangle.lean