OAI/Geometry/Convex/GeneralMahler/Brouwer/Grid.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

A colorful primitive room in grids on the standard simplex.

  1. abbrev OAI.GeneralMahler.Scarf.Grid line 11
  2. lemma OAI.GeneralMahler.Scarf.grid_extend line 14
  3. instance OAI.GeneralMahler.Scarf.(instance at line 25) line 25
  4. def OAI.GeneralMahler.Scarf.place line 29
  5. lemma OAI.GeneralMahler.Scarf.small line 30
  6. lemma OAI.GeneralMahler.Scarf.place_inj line 32
  7. def OAI.GeneralMahler.Scarf.key line 35
  8. lemma OAI.GeneralMahler.Scarf.key_pos line 38
  9. lemma OAI.GeneralMahler.Scarf.key_lt line 40
  10. lemma OAI.GeneralMahler.Scarf.key_order line 47
  11. lemma OAI.GeneralMahler.Scarf.key_inj line 55
  12. def OAI.GeneralMahler.Scarf.grank line 65
  13. lemma OAI.GeneralMahler.Scarf.lkey line 70
  14. lemma OAI.GeneralMahler.Scarf.hkey line 73
  15. lemma OAI.GeneralMahler.Scarf.inex line 77
  16. def OAI.GeneralMahler.Scarf.gridOrder line 82
  17. lemma OAI.GeneralMahler.Scarf.full_approx line 100