OAI/Probability/SKGap/Localization/LiteralSeriesLiftAppend.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKGap.Noncrossing.literalSeries_lift_append line 42
2. lemma OAI.SKGap.Noncrossing.literalSeries_two_prefix line 45
3. lemma OAI.SKGap.Noncrossing.literalSeries_two_suffix line 50
4. lemma OAI.SKGap.Noncrossing.literalSeries_cons_inverse line 55
5. lemma OAI.SKGap.Noncrossing.literalSeries_lift_fun line 60
6. lemma OAI.SKGap.Noncrossing.literalSeries_oneInverse_fun line 63
7. lemma OAI.SKGap.Noncrossing.literalSeries_inverse_diag_fun line 67
8. lemma OAI.SKGap.Noncrossing.literalSeries_inverse_single_append line 71
9. lemma OAI.SKGap.Noncrossing.literalSeries_cons_inverse_fun line 75
10. lemma OAI.SKGap.Noncrossing.literalSeries_inverse_diag_suffix line 80
11. lemma OAI.SKGap.Noncrossing.literalSeries_at_noInverse line 87
12. lemma OAI.SKGap.Noncrossing.literalSeries_at_rightInverse line 103
13. lemma OAI.SKGap.Noncrossing.literalSeries_at_leftInverse line 120
14. lemma OAI.SKGap.Noncrossing.literalSeries_at line 140
15. lemma OAI.SKGap.Noncrossing.exists_diagonals_of_count_zero line 167
16. lemma OAI.SKGap.Noncrossing.wordDiagonal_diags line 180
17. lemma OAI.SKGap.Noncrossing.wordDiagonal_append line 184
18. lemma OAI.SKGap.Noncrossing.wordDiagonal_inverse line 187
19. lemma OAI.SKGap.Noncrossing.literalSeries_base line 190