OAI/Combinatorics/ThinTrees/Continuation/Domain.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Continuation domain.

  1. abbrev OAI.AlgorithmicThinTrees.MetricTests.ResponseSpace line 18
  2. def OAI.AlgorithmicThinTrees.MetricTests.admissible line 20
  3. lemma OAI.AlgorithmicThinTrees.MetricTests.admissible_nonempty line 24
  4. lemma OAI.AlgorithmicThinTrees.MetricTests.admissible_closed line 32
  5. lemma OAI.AlgorithmicThinTrees.MetricTests.admissible_compact line 56
  6. lemma OAI.AlgorithmicThinTrees.MetricTests.admissible_convex line 64
  7. lemma OAI.AlgorithmicThinTrees.MetricTests.lowerCapacity_continuous line 84
  8. lemma OAI.AlgorithmicThinTrees.MetricTests.lowerCapacity_concave line 90
  9. def OAI.AlgorithmicThinTrees.MetricTests.responseSlack line 110
  10. lemma OAI.AlgorithmicThinTrees.MetricTests.responseSlack_continuous line 114
  11. lemma OAI.AlgorithmicThinTrees.MetricTests.responseSlack_concave line 123
  12. lemma OAI.AlgorithmicThinTrees.MetricTests.responseSlack_submodular line 144