OAI/RepresentationTheory/UniversalSquare/Balance/PackingPlans.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Packing Plans.

  1. inductive OAI.Saxl.Balance.PackingPlan line 17
  2. def OAI.Saxl.Balance.PackingPlan.columns line 29
  3. def OAI.Saxl.Balance.PackingPlan.parts line 38
  4. def OAI.Saxl.Balance.PackingPlan.bands line 47
  5. def OAI.Saxl.Balance.PackingPlan.marks line 56
  6. def OAI.Saxl.Balance.PackingPlan.Valid line 58
  7. instance OAI.Saxl.Balance.PackingPlan.(instance at line 68) line 68
  8. theorem OAI.Saxl.Balance.PackingPlan.realize line 78
  9. theorem OAI.UniversalTensorSquare.packingPlan_pos line 129