OAI/Computability/PerfectCompleteness/Sampling/OriginalUniformCutBase.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PerfectCompleteness.OriginalUniformCutBase.valuesChildrenFintype line 20
  2. def OAI.PerfectCompleteness.OriginalUniformCutBase.assembleEquiv line 28
  3. theorem OAI.PerfectCompleteness.OriginalUniformCutBase.uniform_assemble_law line 43
  4. theorem OAI.PerfectCompleteness.OriginalUniformCutBase.uniform_bucket_assemble_law line 56
  5. theorem OAI.PerfectCompleteness.OriginalUniformCutBase.uniform_pushforward_reindex line 87
  6. abbrev OAI.PerfectCompleteness.OriginalUniformCutBase.ReflRecord line 104
  7. def OAI.PerfectCompleteness.OriginalUniformCutBase.reflRecordEquiv line 108
  8. def OAI.PerfectCompleteness.OriginalUniformCutBase.renderRecord line 113
  9. theorem OAI.PerfectCompleteness.OriginalUniformCutBase.renderRecord_equiv line 119
  10. theorem OAI.PerfectCompleteness.OriginalUniformCutBase.uniform_renderRecord line 125
  11. theorem OAI.PerfectCompleteness.OriginalUniformCutBase.uniform_reconstructRecord_refl line 141