OAI/Geometry/Convex/GeneralMahler/Segment/Element.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Elementary small angle quantitative inequalities.

  1. lemma OAI.GeneralMahler.SCal.SE.integUp line 10
  2. lemma OAI.GeneralMahler.SCal.SE.cs_L4 line 19
  3. lemma OAI.GeneralMahler.SCal.SE.sn_H5 line 28
  4. lemma OAI.GeneralMahler.SCal.SE.cs6 line 36
  5. lemma OAI.GeneralMahler.SCal.SE.snsq line 46
  6. lemma OAI.GeneralMahler.SCal.SE.sinDif line 51
  7. lemma OAI.GeneralMahler.SCal.SE.ch0 line 73
  8. lemma OAI.GeneralMahler.SCal.SE.ch2 line 78
  9. lemma OAI.GeneralMahler.SCal.SE.sh3 line 85
  10. lemma OAI.GeneralMahler.SCal.SE.cshH line 93
  11. lemma OAI.GeneralMahler.SCal.SE.sinhH line 115
  12. lemma OAI.GeneralMahler.SCal.SE.coth_est line 126
  13. lemma OAI.GeneralMahler.SCal.SE.smallConst line 146