OAI/Combinatorics/ThinTrees/Continuation/PartitionGeometry.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

Partition geometry.

  1. def OAI.AlgorithmicThinTrees.Partitions.block line 18
  2. lemma OAI.AlgorithmicThinTrees.Partitions.mem_block line 20
  3. lemma OAI.AlgorithmicThinTrees.Partitions.self_mem_block line 23
  4. lemma OAI.AlgorithmicThinTrees.Partitions.block_eq_iff line 26
  5. lemma OAI.AlgorithmicThinTrees.Partitions.block_block line 35
  6. lemma OAI.AlgorithmicThinTrees.Partitions.block_mono line 38
  7. def OAI.AlgorithmicThinTrees.Partitions.parts line 42
  8. lemma OAI.AlgorithmicThinTrees.Partitions.block_mem_parts line 44
  9. lemma OAI.AlgorithmicThinTrees.Partitions.mem_parts line 47
  10. lemma OAI.AlgorithmicThinTrees.Partitions.parts_top line 50
  11. lemma OAI.AlgorithmicThinTrees.Partitions.parts_disjoint line 56
  12. lemma OAI.AlgorithmicThinTrees.Partitions.parts_cover line 66
  13. lemma OAI.AlgorithmicThinTrees.Partitions.partCount_pos line 71
  14. lemma OAI.AlgorithmicThinTrees.Partitions.partCount_top line 74
  15. lemma OAI.AlgorithmicThinTrees.Partitions.two_le_partCount line 81
  16. lemma OAI.AlgorithmicThinTrees.Partitions.parts_partition line 88
  17. def OAI.AlgorithmicThinTrees.Partitions.toChain line 99
  18. lemma OAI.AlgorithmicThinTrees.Partitions.toChain_block line 106
  19. def OAI.AlgorithmicThinTrees.Partitions.crossing line 110
  20. lemma OAI.AlgorithmicThinTrees.Partitions.mem_crossing line 113
  21. lemma OAI.AlgorithmicThinTrees.Partitions.toChain_crossing line 116
  22. lemma OAI.AlgorithmicThinTrees.Partitions.capacity_eq_sum line 121
  23. lemma OAI.AlgorithmicThinTrees.Partitions.enumerate_chain line 128