OAI/RepresentationTheory/Saxl/HorizontalRemoval.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Saxl.rowPrefix line 10
  2. def OAI.Saxl.Dominates line 12
  3. lemma OAI.Saxl.rowLen_zero_of_height_le line 14
  4. lemma OAI.Saxl.rowPrefix_eq_card line 22
  5. def OAI.Saxl.stripRow line 34

    Source comment

    Tallest-column bottom deletion, expressed by interlacing rows.
    def stripRow (μ : YoungDiagram) (t i : ℕ) := μ.rowLen i - t + min t (μ.rowLen (i+1))
  6. lemma OAI.Saxl.stripRow_bounds line 36
  7. lemma OAI.Saxl.stripRow_antitone line 42
  8. def OAI.Saxl.stripRemove line 47
  9. lemma OAI.Saxl.mem_stripRemove line 55
  10. lemma OAI.Saxl.stripRemove_rowLen line 62
  11. lemma OAI.Saxl.stripRemove_le line 71
  12. lemma OAI.Saxl.stripRemove_horizontal line 75
  13. lemma OAI.Saxl.stripRemove_prefix line 93
  14. lemma OAI.Saxl.stripRemove_card line 107
  15. lemma OAI.Saxl.stripRemove_full line 118
  16. lemma OAI.Saxl.rowPrefix_succ line 127
  17. lemma OAI.Saxl.rowPrefix_le_card line 131
  18. lemma OAI.Saxl.rowPrefix_mono line 135
  19. def OAI.Saxl.rowTruncate line 139
  20. lemma OAI.Saxl.mem_rowTruncate line 146
  21. lemma OAI.Saxl.rowTruncate_rowLen line 151
  22. lemma OAI.Saxl.rowTruncate_height line 161
  23. lemma OAI.Saxl.rowTruncate_prefix line 166
  24. lemma OAI.Saxl.rowTruncate_card line 172
  25. lemma OAI.Saxl.dominates_stripRemove_last line 176