OAI/Combinatorics/IndependentSets/Reduction/SubchainView.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.LargeIndependentSets.SubchainView line 9
2. def OAI.LargeIndependentSets.chainView line 14
3. lemma OAI.LargeIndependentSets.occurrenceTuple_local_left line 19
4. lemma OAI.LargeIndependentSets.occurrenceTuple_local_right line 28
5. lemma OAI.LargeIndependentSets.chainComposite_local line 37
6. lemma OAI.LargeIndependentSets.chainView_local_left line 49
7. lemma OAI.LargeIndependentSets.chainView_local_right line 59
8. abbrev OAI.LargeIndependentSets.SubchainCoord line 69
9. def OAI.LargeIndependentSets.leftEntry line 72
10. def OAI.LargeIndependentSets.rightEntry line 74
11. lemma OAI.LargeIndependentSets.leftEntry_spec line 77
12. lemma OAI.LargeIndependentSets.rightEntry_spec line 85
13. def OAI.LargeIndependentSets.terminalList line 93
14. lemma OAI.LargeIndependentSets.terminal_intersection_decodes line 98
15. def OAI.LargeIndependentSets.ownQuestionList line 119
16. lemma OAI.LargeIndependentSets.ownQuestionList_apply line 123
17. lemma OAI.LargeIndependentSets.ownQuestionList_card line 129
18. theorem OAI.LargeIndependentSets.separated_lists_conditioned line 134