OAI/Combinatorics/ThinTrees/Continuation/PartitionLocalConnectivity.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Partition local connectivity.

  1. def OAI.AlgorithmicThinTrees.Partitions.split line 18
  2. lemma OAI.AlgorithmicThinTrees.Partitions.split_iff line 21
  3. lemma OAI.AlgorithmicThinTrees.Partitions.split_strict line 26
  4. lemma OAI.AlgorithmicThinTrees.Partitions.crossing_split line 42
  5. lemma OAI.AlgorithmicThinTrees.Partitions.crossing_split_disjoint line 58
  6. lemma OAI.AlgorithmicThinTrees.Partitions.capacity_split line 66
  7. lemma OAI.AlgorithmicThinTrees.Partitions.split_capacity_lower line 73
  8. def OAI.AlgorithmicThinTrees.Partitions.active line 87
  9. lemma OAI.AlgorithmicThinTrees.Partitions.mem_active line 89
  10. lemma OAI.AlgorithmicThinTrees.Partitions.capacity_active_upper line 92
  11. lemma OAI.AlgorithmicThinTrees.Partitions.restrict_induced line 112
  12. lemma OAI.AlgorithmicThinTrees.Partitions.restrict_internal_cut_card line 123
  13. theorem OAI.AlgorithmicThinTrees.Partitions.near_tight_locally_connected line 133