OAI/NumberTheory/Jacobsthal/Partitions/MeshBoundaryGeometry.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.NumberTheoryLean.MeshRatioLabels.binCount line 16
  2. abbrev OAI.Erdos970.NumberTheoryLean.MeshRatioLabels.Label line 17
  3. def OAI.Erdos970.NumberTheoryLean.MeshRatioLabels.cemeteryLabel line 19
  4. def OAI.Erdos970.NumberTheoryLean.MeshRatioLabels.ratioLabel line 21
  5. theorem OAI.Erdos970.NumberTheoryLean.MeshRatioLabels.ratioLabel_measurable line 24
  6. theorem OAI.Erdos970.NumberTheoryLean.MeshRatioLabels.ratioLabel_val line 29
  7. theorem OAI.Erdos970.NumberTheoryLean.MeshRatioLabels.ratioLabel_ne_cemetery line 36
  8. theorem OAI.Erdos970.NumberTheoryLean.MeshRatioLabels.ratioLabel_eq_iff line 45
  9. theorem OAI.Erdos970.NumberTheoryLean.MeshRatioLabels.matching_ratios_close line 49
  10. theorem OAI.Erdos970.NumberTheoryLean.MeshRatioLabels.label_card_le line 56
  11. def OAI.Erdos970.NumberTheoryLean.MeshBoundaryGeometry.lowerEdge line 74
  12. def OAI.Erdos970.NumberTheoryLean.MeshBoundaryGeometry.upperEdge line 75
  13. def OAI.Erdos970.NumberTheoryLean.MeshBoundaryGeometry.fullCell line 77
  14. def OAI.Erdos970.NumberTheoryLean.MeshBoundaryGeometry.lowerPacket line 80
  15. def OAI.Erdos970.NumberTheoryLean.MeshBoundaryGeometry.upperPacket line 81
  16. theorem OAI.Erdos970.NumberTheoryLean.MeshBoundaryGeometry.noninterior_in_packets line 83
  17. theorem OAI.Erdos970.NumberTheoryLean.MeshBoundaryGeometry.lowerPacket_width line 103
  18. theorem OAI.Erdos970.NumberTheoryLean.MeshBoundaryGeometry.upperPacket_width line 108
  19. theorem OAI.Erdos970.NumberTheoryLean.MeshBoundaryGeometry.clipPacket line 113
  20. theorem OAI.Erdos970.NumberTheoryLean.MeshBoundaryGeometry.clipped_packet_width line 122