OAI/Combinatorics/FiniteCircle/RandomCodes.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.FiniteCircle.SmallHoles line 13
  2. abbrev OAI.FiniteCircle.DenseParameters line 14
  3. instance OAI.FiniteCircle.(instance at line 16) line 16
  4. def OAI.FiniteCircle.denseList line 18
  5. theorem OAI.FiniteCircle.denseList_sorted line 21
  6. theorem OAI.FiniteCircle.exists_denseParameters line 25
  7. def OAI.FiniteCircle.StrongLocal line 53
  8. abbrev OAI.FiniteCircle.DenseWitness line 63
  9. def OAI.FiniteCircle.badDenseWitness line 65
  10. theorem OAI.FiniteCircle.card_badDenseWitness_le line 72
  11. theorem OAI.FiniteCircle.card_denseWitness_le line 116
  12. theorem OAI.FiniteCircle.dense_union_numerics line 133
  13. theorem OAI.FiniteCircle.exists_coding_width line 166
  14. theorem OAI.FiniteCircle.exists_strongLocal line 192