OAI/Combinatorics/SharpRamsey/Exposure/PreparedMixture.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.SharpLogRamsey.Selection.Windows.PositiveHistory line 22
2. def OAI.SharpLogRamsey.Selection.Windows.mixedPrepared line 27
3. def OAI.SharpLogRamsey.Selection.Windows.attachedPrepared line 29
4. lemma OAI.SharpLogRamsey.Selection.Windows.attachedPrepared_tuple line 35
5. lemma OAI.SharpLogRamsey.Selection.Windows.attachedPrepared_original line 48
6. lemma OAI.SharpLogRamsey.Selection.Windows.attachedPrepared_left line 53
7. theorem OAI.SharpLogRamsey.Selection.Windows.attachedPrepared_loss line 59