OAI/Analysis/TriangularHilbert/GridCell.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.TriangularHilbert.gridCell line 13
  2. def OAI.TriangularHilbert.gridIndex line 14
  3. def OAI.TriangularHilbert.gridPoint line 15
  4. lemma OAI.TriangularHilbert.gridCell_mem_iff line 17
  5. lemma OAI.TriangularHilbert.gridPoint_le line 30
  6. lemma OAI.TriangularHilbert.gridPoint_lt_add line 33
  7. lemma OAI.TriangularHilbert.abs_gridPoint_sub_lt line 38
  8. lemma OAI.TriangularHilbert.volume_gridCell line 42
  9. def OAI.TriangularHilbert.gridRect line 47
  10. def OAI.TriangularHilbert.gridLift line 49
  11. lemma OAI.TriangularHilbert.gridRect_mem_iff line 52
  12. lemma OAI.TriangularHilbert.gridLift_eq line 56
  13. lemma OAI.TriangularHilbert.gridLift_comp line 88
  14. lemma OAI.TriangularHilbert.measurableSet_gridRect line 94
  15. lemma OAI.TriangularHilbert.volume_gridRect line 97
  16. lemma OAI.TriangularHilbert.integral_gridLift line 101