OAI/Combinatorics/ThinTrees/Metric/CompactDuality.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Metric compact duality.

  1. lemma OAI.AlgorithmicThinTrees.MetricTests.average_antitone line 17
  2. lemma OAI.AlgorithmicThinTrees.MetricTests.average_smul line 23
  3. lemma OAI.AlgorithmicThinTrees.MetricTests.average_continuousAt line 31
  4. def OAI.AlgorithmicThinTrees.MetricTests.pdBox line 41
  5. lemma OAI.AlgorithmicThinTrees.MetricTests.pdBox_pd line 44
  6. lemma OAI.AlgorithmicThinTrees.MetricTests.pdBox_closed line 47
  7. lemma OAI.AlgorithmicThinTrees.MetricTests.pdBox_bounded line 51
  8. lemma OAI.AlgorithmicThinTrees.MetricTests.pdBox_compact line 65
  9. lemma OAI.AlgorithmicThinTrees.MetricTests.pdBox_objective_closed line 68
  10. theorem OAI.AlgorithmicThinTrees.MetricTests.metric_shortcut_of_trace_bound line 87