OAI/Analysis/LipschitzFree/Evaluation.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Evaluation isometries, completeness, and closed-span induction

  1. def OAI.DiscreteFree.distanceTest line 18
  2. theorem OAI.DiscreteFree.distanceTest_apply line 22
  3. theorem OAI.DiscreteFree.distanceTest_norm_le line 25
  4. theorem OAI.DiscreteFree.evaluation_sub_norm line 30
  5. theorem OAI.DiscreteFree.evaluation_norm line 40
  6. theorem OAI.DiscreteFree.delta_base line 43
  7. theorem OAI.DiscreteFree.delta_sub_norm line 47
  8. theorem OAI.DiscreteFree.delta_norm line 50
  9. theorem OAI.DiscreteFree.delta_isometry line 52
  10. instance OAI.DiscreteFree.(instance at line 57) line 57
  11. theorem OAI.DiscreteFree.freeSpace_induction line 60