OAI/Analysis/PrefixRadix/Intervals.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Closed prefix intervals and quantitative separation.

  1. def OAI.PrefixFlows.Radix.System.finiteCode line 14
  2. def OAI.PrefixFlows.Radix.System.interval line 18
  3. theorem OAI.PrefixFlows.Radix.System.code_prepend line 22
  4. theorem OAI.PrefixFlows.Radix.System.code_blank_tail line 34
  5. theorem OAI.PrefixFlows.Radix.System.code_mem_interval line 39
  6. theorem OAI.PrefixFlows.Radix.System.finite_bounds line 47
  7. theorem OAI.PrefixFlows.Radix.System.interval_subset_unit line 65
  8. theorem OAI.PrefixFlows.Radix.System.mem_interval_cons line 71
  9. theorem OAI.PrefixFlows.Radix.System.incompatible_intervals_separated line 102
  10. theorem OAI.PrefixFlows.Radix.System.incompatible_intervals_disjoint line 141