OAI/NumberTheory/OrdinaryCorrelations/HighTrace/Precedes.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.PrivateFamily.Case.Precedes line 22
2. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.PrivateFamily.Case.variable line 27
3. def OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.PrivateFamily.caseTest line 32
4. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.PrivateFamily.caseTest_selected line 44
5. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.PrivateFamily.caseTest_valid line 51
6. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.PrivateFamily.caseTest_future_absent line 75
7. lemma OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.PrivateFamily.variable_injective_on_case line 91
8. theorem OAI.OrdinaryCorrelations.GraphKernel.PrimeSystem.PrivateFamily.triangular_tests line 113