OAI/Combinatorics/ThinTrees/Flow/RootedRelaxation.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Rooted relaxation.

  1. lemma OAI.AlgorithmicThinTrees.Orientations.parts_card line 16
  2. lemma OAI.AlgorithmicThinTrees.Orientations.parts_sum_card line 32
  3. lemma OAI.AlgorithmicThinTrees.Orientations.block_eq_of_part line 42
  4. lemma OAI.AlgorithmicThinTrees.Orientations.internal_partition_accounting line 47
  5. structure OAI.AlgorithmicThinTrees.Orientations.FlowPoint line 68
  6. def OAI.AlgorithmicThinTrees.Orientations.FlowPoint.Feasible line 73
  7. lemma OAI.AlgorithmicThinTrees.Orientations.sum_root_budget line 80
  8. lemma OAI.AlgorithmicThinTrees.Orientations.internal_flow_bound line 87
  9. lemma OAI.AlgorithmicThinTrees.Orientations.flow_partition_bound line 100
  10. theorem OAI.AlgorithmicThinTrees.Orientations.relaxed_flow_implies_partitions line 117