OAI/Combinatorics/BalancedRyser/Probability/ForwardDependencyExtraction.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Balanced.ForwardDependencyExtraction.exists_forward_coloring line 10
2. theorem OAI.Balanced.ForwardDependencyExtraction.exists_forward_subset line 89
3. theorem OAI.Balanced.ForwardDependencyExtraction.exists_large_forward_subset line 104
4. theorem OAI.Balanced.ForwardDependencyExtraction.wellFounded_on_of_forward line 134
5. theorem OAI.Balanced.ForwardDependencyExtraction.extract_three_of_eight line 142
6. theorem OAI.Balanced.ForwardDependencyExtraction.extract_two_of_four line 154