OAI/Combinatorics/RamseyFive/Iteration/TerminalStream.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SharpRamseyFive.SelectedTuple.eventually_no_terminal_stream line 15
2. structure OAI.SharpRamseyFive.SelectedTuple.PolarState line 63
3. def OAI.SharpRamseyFive.SelectedTuple.PolarState.of line 80
4. theorem OAI.SharpRamseyFive.SelectedTuple.eventually_polar_compression line 90
5. theorem OAI.SharpRamseyFive.SelectedTuple.eventually_polar_terminal line 118
6. lemma OAI.SharpRamseyFive.SelectedTuple.iid_uniform_mass line 137
7. def OAI.SharpRamseyFive.SelectedTuple.initialSelectedStream line 141
8. def OAI.SharpRamseyFive.SelectedTuple.firstWitness line 168
9. lemma OAI.SharpRamseyFive.SelectedTuple.firstWitness_spec line 176
10. theorem OAI.SharpRamseyFive.SelectedTuple.initial_selected_exists line 183