OAI/Combinatorics/ThinTrees/Continuation/Start.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Continuation start.

  1. lemma OAI.AlgorithmicThinTrees.MetricTests.rankOne_le_laplacian line 15
  2. lemma OAI.AlgorithmicThinTrees.MetricTests.initial_resistance_le_one line 22
  3. lemma OAI.AlgorithmicThinTrees.MetricTests.initial_ramp line 29
  4. lemma OAI.AlgorithmicThinTrees.MetricTests.packing_connected line 41
  5. lemma OAI.AlgorithmicThinTrees.MetricTests.packing_count_le_edges line 47
  6. lemma OAI.AlgorithmicThinTrees.MetricTests.packing_partition_slack line 58
  7. def OAI.AlgorithmicThinTrees.MetricTests.RationalStep.initial line 78
  8. lemma OAI.AlgorithmicThinTrees.MetricTests.RationalStep.initial_invariant line 81