OAI/Combinatorics/ThinTrees/Continuation/PartitionUncrossing.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Partition uncrossing.

  1. def OAI.AlgorithmicThinTrees.Partitions.Certificates line 18
  2. lemma OAI.AlgorithmicThinTrees.Partitions.certificates_isClosed line 21
  3. lemma OAI.AlgorithmicThinTrees.Partitions.certificates_compact line 34
  4. def OAI.AlgorithmicThinTrees.Partitions.uncrossWeight line 44
  5. lemma OAI.AlgorithmicThinTrees.Partitions.uncrossWeight_nonneg line 49
  6. lemma OAI.AlgorithmicThinTrees.Partitions.uncrossWeight_dot line 67
  7. lemma OAI.AlgorithmicThinTrees.Partitions.uncrossWeight_sum line 72
  8. theorem OAI.AlgorithmicThinTrees.Partitions.chain_certificate line 77
  9. theorem OAI.AlgorithmicThinTrees.Partitions.feasible_of_chain_feasible line 111