OAI/Combinatorics/BalancedRyser/Construction/RootChildPartition.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Balanced.RootChildPartition.DisjointRoots line 14
2. theorem OAI.Balanced.RootChildPartition.exists_maximal_roots line 17
3. theorem OAI.Balanced.RootChildPartition.exists_roots_of_small_shared line 53
4. theorem OAI.Balanced.RootChildPartition.disjointRoots_of_zero_reuse line 78
5. theorem OAI.Balanced.RootChildPartition.exists_roots_of_large_shared line 92
6. theorem OAI.Balanced.RootChildPartition.exists_root_child_partition line 171
7. theorem OAI.Balanced.RootChildPartition.partition_image line 186
8. theorem OAI.Balanced.RootChildPartition.exists_pattern_roots line 210
9. theorem OAI.Balanced.RootChildPartition.exists_uniform_prescribed_roots line 239