Commit 2023-06-07 04:25 bb248dea

View on Github →

feat: port Analysis.SpecialFunctions.Trigonometric.Bounds (#4768)

Estimated changes

Modified Mathlib.lean

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

added theorem Real.cos_le_one_div_sqrt_sq_add_one

added theorem Real.cos_lt_one_div_sqrt_sq_add_one

added theorem Real.deriv_tan_sub_id

added theorem Real.le_tan

added theorem Real.lt_tan

added theorem Real.sin_gt_sub_cube

added theorem Real.sin_lt