OAI/Combinatorics/SumProduct/Alignment/MenuLiteral01.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.SourceMenuLiteral.CosetPiece line 56
  2. def OAI.SourceMenuLiteral.CosetPiece.eval line 67
  3. def OAI.SourceMenuLiteral.CosetPiece.lift line 69
  4. lemma OAI.SourceMenuLiteral.CosetPiece.lift_eval line 77
  5. def OAI.SourceMenuLiteral.raiseChart line 84
  6. def OAI.SourceMenuLiteral.raiseMenu line 93
  7. def OAI.SourceMenuLiteral.CosetPiece.raise line 96
  8. structure OAI.SourceMenuLiteral.ModelsSystem line 101
  9. def OAI.SourceMenuLiteral.ModelsSystem.lift line 113
  10. def OAI.SourceMenuLiteral.ModelsSystem.raise line 122
  11. theorem OAI.SourceMenuLiteral.charted_finite_menu_alignment line 130