OAI/Analysis/RecorderRadix/Intervals.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

Odd radix digits and separated one-letter and two-letter intervals.

  1. def OAI.Solenoidal.Radix.base line 9
  2. def OAI.Solenoidal.Radix.digit line 11
  3. def OAI.Solenoidal.Radix.pushDigit line 13
  4. def OAI.Solenoidal.Radix.pop line 16
  5. def OAI.Solenoidal.Radix.first line 18
  6. def OAI.Solenoidal.Radix.two line 21
  7. theorem OAI.Solenoidal.Radix.base_three_le line 24
  8. theorem OAI.Solenoidal.Radix.base_pos line 29
  9. theorem OAI.Solenoidal.Radix.digit_bounds line 31
  10. theorem OAI.Solenoidal.Radix.pop_prefix line 37
  11. theorem OAI.Solenoidal.Radix.prefix_pop line 42
  12. theorem OAI.Solenoidal.Radix.prefix_le_prefix_iff line 47
  13. theorem OAI.Solenoidal.Radix.prefix_image_Icc line 52
  14. theorem OAI.Solenoidal.Radix.prefix_image_unit line 66
  15. theorem OAI.Solenoidal.Radix.prefix_image_first line 69
  16. theorem OAI.Solenoidal.Radix.pop_image_first line 72
  17. theorem OAI.Solenoidal.Radix.lower_nonneg line 77
  18. theorem OAI.Solenoidal.Radix.upper_le_one line 81
  19. theorem OAI.Solenoidal.Radix.first_ordered_gap line 87
  20. theorem OAI.Solenoidal.Radix.first_separated line 96
  21. theorem OAI.Solenoidal.Radix.prefix_gap line 104
  22. theorem OAI.Solenoidal.Radix.two_gap_same line 111
  23. theorem OAI.Solenoidal.Radix.two_gap_first line 115
  24. theorem OAI.Solenoidal.Radix.two_separated line 127