OAI/Combinatorics/FiniteCircle/ExcludedSeparation.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FiniteCircle.excludedPhaseHom line 9
  2. theorem OAI.FiniteCircle.excludedPhaseHom_apply line 15
  3. theorem OAI.FiniteCircle.excludedPhaseHom_natCast line 21
  4. def OAI.FiniteCircle.excludedCost line 33
  5. theorem OAI.FiniteCircle.excludedCost_le_half line 41
  6. theorem OAI.FiniteCircle.excluded_active_average_lower line 51
  7. theorem OAI.FiniteCircle.excluded_inactive_average_lower line 102
  8. theorem OAI.FiniteCircle.excluded_minimizer_options line 131
  9. def OAI.FiniteCircle.excludedTags line 155
  10. theorem OAI.FiniteCircle.length_excludedTags line 157
  11. theorem OAI.FiniteCircle.mem_excludedTags line 160
  12. theorem OAI.FiniteCircle.nodup_excludedTags line 163
  13. theorem OAI.FiniteCircle.excludedWord_succ line 167
  14. def OAI.FiniteCircle.excludedLength line 177
  15. theorem OAI.FiniteCircle.length_excludedWord line 181
  16. theorem OAI.FiniteCircle.shiftExcludedState_zero line 200
  17. theorem OAI.FiniteCircle.shiftExcludedState_add line 206
  18. theorem OAI.FiniteCircle.shiftExcludedState_change_base line 214
  19. def OAI.FiniteCircle.excludedRow line 222
  20. theorem OAI.FiniteCircle.length_excludedRow line 227
  21. theorem OAI.FiniteCircle.segment_excludedWord line 238
  22. theorem OAI.FiniteCircle.tag_get_excludedWord line 250
  23. theorem OAI.FiniteCircle.excludedLength_pos line 272
  24. theorem OAI.FiniteCircle.excluded_separation line 283