OAI/Analysis/LipschitzFree/ScalarTests.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Finite-state records and opposing scalar Lipschitz tests

  1. def OAI.DiscreteFree.MetricBlock.Compatible line 20
  2. def OAI.DiscreteFree.MetricBlock.Transition line 23
  3. def OAI.DiscreteFree.MetricBlock.supportColors line 25
  4. theorem OAI.DiscreteFree.MetricBlock.supportColors_card line 29
  5. theorem OAI.DiscreteFree.MetricBlock.compatible_color line 35
  6. theorem OAI.DiscreteFree.MetricBlock.transition_card line 41
  7. def OAI.DiscreteFree.MetricBlock.exceptionSet line 59
  8. theorem OAI.DiscreteFree.MetricBlock.exceptional_unique_good line 66
  9. theorem OAI.DiscreteFree.MetricBlock.exceptional_endpoint line 74
  10. theorem OAI.DiscreteFree.MetricBlock.positive_bump_compatible line 94
  11. theorem OAI.DiscreteFree.MetricBlock.edge_test line 119