OAI/Analysis/LipschitzFree/Attachment.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Attachment-length estimates and label compatibility

  1. theorem OAI.DiscreteFree.PortGraph.near_trans line 17
  2. def OAI.DiscreteFree.MetricBlock.ShortRelation line 27
  3. theorem OAI.DiscreteFree.MetricBlock.short_self line 33
  4. theorem OAI.DiscreteFree.MetricBlock.short_trans line 39
  5. theorem OAI.DiscreteFree.MetricBlock.short_edge line 46
  6. theorem OAI.DiscreteFree.MetricBlock.short_distance line 73
  7. theorem OAI.DiscreteFree.MetricBlock.short_mono line 85
  8. theorem OAI.DiscreteFree.MetricBlock.short_finite line 94
  9. theorem OAI.DiscreteFree.MetricBlock.short_card_le line 109
  10. theorem OAI.DiscreteFree.MetricBlock.closedBall_finite line 135
  11. theorem OAI.DiscreteFree.MetricBlock.closedBall_card_le line 145
  12. theorem OAI.DiscreteFree.MetricBlock.label_occurs line 161
  13. theorem OAI.DiscreteFree.MetricBlock.label_support_card line 168
  14. theorem OAI.DiscreteFree.MetricBlock.color_in_support line 177