OAI/Probability/SKGap/Localization/StartedPrefix.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKGapCutoff.Recipe.OrdinaryData.started_evaluation_prefix_eq line 15
2. lemma OAI.SKGapCutoff.Recipe.OrdinaryData.appendProduct_started_prefix line 48
3. lemma OAI.SKGapCutoff.Recipe.OrdinaryData.appendProduct_started_source line 64
4. lemma OAI.SKGapCutoff.Recipe.OrdinaryData.appendProduct_started_partial line 81
5. lemma OAI.SKGapCutoff.Recipe.OrdinaryData.appendAuxiliary_started_prefix line 115
6. lemma OAI.SKGapCutoff.Recipe.OrdinaryData.appendAuxiliary_started_source line 124
7. lemma OAI.SKGapCutoff.Recipe.OrdinaryData.Admissible.startedPartial line 135