OAI/Combinatorics/RamseyFive/Entropy/MetadataAlphabet.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SharpRamseyFive.Metadata.TwoListCode line 8
  2. instance OAI.SharpRamseyFive.Metadata.(instance at line 12) line 12
  3. lemma OAI.SharpRamseyFive.Metadata.card_TwoListCode line 15
  4. def OAI.SharpRamseyFive.Metadata.ListProfile line 21
  5. instance OAI.SharpRamseyFive.Metadata.(instance at line 23) line 23
  6. def OAI.SharpRamseyFive.Metadata.TrainingCode line 26
  7. instance OAI.SharpRamseyFive.Metadata.(instance at line 29) line 29
  8. instance OAI.SharpRamseyFive.Metadata.(instance at line 32) line 32
  9. lemma OAI.SharpRamseyFive.Metadata.card_profile line 42
  10. theorem OAI.SharpRamseyFive.Metadata.card_TrainingCode line 46
  11. theorem OAI.SharpRamseyFive.Metadata.log_card_TrainingCode line 66