OAI/Combinatorics/Progressions/Sampling/SamplerSeparatedVariables.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.samplerSeparatedVariable line 13
2. theorem OAI.Erdos3.samplerSeparatedVariable_common line 23
3. theorem OAI.Erdos3.samplerSeparatedVariable_inactive line 27
4. theorem OAI.Erdos3.samplerSeparatedVariable_active line 33
5. def OAI.Erdos3.samplerFrozenRaw line 39
6. theorem OAI.Erdos3.samplerSeparatedValues_eq_extend line 46
7. theorem OAI.Erdos3.eval_rename_samplerSeparatedVariable line 68