OAI/RepresentationTheory/PartialPermutation/RowBounds.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PartialPermutation.Tableau.topPrefix line 13
2. instance OAI.PartialPermutation.Tableau.(instance at line 16) line 16
3. lemma OAI.PartialPermutation.Tableau.topPrefix_lower line 19
4. def OAI.PartialPermutation.Tableau.topPrefixEquiv line 24
5. lemma OAI.PartialPermutation.Tableau.topPrefix_card line 31
6. def OAI.PartialPermutation.Tableau.topRowEquiv line 35
7. lemma OAI.PartialPermutation.Tableau.lower_card line 41
8. lemma OAI.PartialPermutation.Tableau.topRow_le_card line 48
9. lemma OAI.PartialPermutation.Tableau.prefix_upper_card line 54
10. def OAI.PartialPermutation.Tableau.lowerInUpperEquiv line 58
11. lemma OAI.PartialPermutation.Tableau.row_interleaving_lower_bound line 65
12. lemma OAI.PartialPermutation.Tableau.secondRow_le_lower line 91