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

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

§08 chord kernel W for signed comparison.

  1. def OAI.GeneralMahler.SCal.SE.leng line 11
  2. def OAI.GeneralMahler.SCal.SE.shv line 12
  3. def OAI.GeneralMahler.SCal.SE.cθ line 13
  4. def OAI.GeneralMahler.SCal.SE.omega line 14
  5. lemma OAI.GeneralMahler.SCal.SE.lnv line 15
  6. lemma OAI.GeneralMahler.SCal.SE.θ_occ line 16
  7. lemma OAI.GeneralMahler.SCal.SE.om0 line 22
  8. lemma OAI.GeneralMahler.SCal.SE.cX0 line 30
  9. lemma OAI.GeneralMahler.SCal.SE.omCont line 48
  10. lemma OAI.GeneralMahler.SCal.SE.ch_err line 54