OAI/Combinatorics/BalancedRyser/Local/AlignedTokenPointLaw.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Balanced.Local.TokenExposure.tupleDirections line 15
  2. theorem OAI.Balanced.Local.TokenExposure.tupleDirections_injective line 20
  3. theorem OAI.Balanced.Local.TokenExposure.tupleDirections_adjacent line 27
  4. theorem OAI.Balanced.Local.TokenExposure.tupleDirections_ne_target line 34
  5. def OAI.Balanced.Local.TokenExposure.pointKernel line 41
  6. theorem OAI.Balanced.Local.TokenExposure.pointKernel_dependsOnExposed line 49
  7. theorem OAI.Balanced.Local.TokenExposure.pointKernel_fixed_dependsOnExposed line 71