OAI/Analysis/LipschitzFree/BoxLabels.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Finite box labels with the supremum metric

  1. def OAI.DiscreteFree.BoxLabel line 16
  2. instance OAI.DiscreteFree.(instance at line 18) line 18
  3. def OAI.DiscreteFree.BoxLabel.distance line 24
  4. theorem OAI.DiscreteFree.BoxLabel.coord_le line 26
  5. theorem OAI.DiscreteFree.BoxLabel.distance_le_iff line 29
  6. theorem OAI.DiscreteFree.BoxLabel.distance_self line 33
  7. theorem OAI.DiscreteFree.BoxLabel.distance_comm line 36
  8. theorem OAI.DiscreteFree.BoxLabel.distance_triangle line 39
  9. theorem OAI.DiscreteFree.BoxLabel.eq_of_distance_zero line 45
  10. theorem OAI.DiscreteFree.BoxLabel.distance_bound line 50
  11. instance OAI.DiscreteFree.BoxLabel.(instance at line 58) line 58
  12. theorem OAI.DiscreteFree.BoxLabel.dist_eq line 65
  13. theorem OAI.DiscreteFree.BoxLabel.cast_nat_dist line 67
  14. theorem OAI.DiscreteFree.BoxLabel.real_coord_le line 76
  15. theorem OAI.DiscreteFree.BoxLabel.dist_eq_real_sup line 81