OAI/Computability/PerfectCompleteness/Construction/WholeCutLocalityLemmas.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PerfectCompleteness.WholeCutLocality.F2 line 13
  2. theorem OAI.PerfectCompleteness.WholeCutLocality.evaluate_root line 19
  3. theorem OAI.PerfectCompleteness.WholeCutLocality.evaluate_selected line 26
  4. theorem OAI.PerfectCompleteness.WholeCutLocality.evaluate_ordinary line 35
  5. theorem OAI.PerfectCompleteness.WholeCutLocality.joint_eq_of_view_eq line 45
  6. theorem OAI.PerfectCompleteness.WholeCutLocality.joint_eq_of_grouped_zero line 140
  7. theorem OAI.PerfectCompleteness.WholeCutLocality.fullJoint_eq_of_grouped_zero line 153
  8. def OAI.PerfectCompleteness.WholeCutKeyLocality.query line 188
  9. theorem OAI.PerfectCompleteness.WholeCutKeyLocality.query_constant line 192
  10. def OAI.PerfectCompleteness.WholeCutKeyLocality.retainedQuery line 201
  11. theorem OAI.PerfectCompleteness.WholeCutKeyLocality.retainedQuery_eq_of_extension line 206
  12. theorem OAI.PerfectCompleteness.WholeCutKeyLocality.query_factor line 217
  13. theorem OAI.PerfectCompleteness.WholeCutKeyLocality.clean_position_dropped line 224
  14. theorem OAI.PerfectCompleteness.WholeCutKeyLocality.key_eq_retained line 235
  15. theorem OAI.PerfectCompleteness.WholeCutKeyLocality.label_eq_retained line 247
  16. theorem OAI.PerfectCompleteness.WholeCutKeyLocality.response_eq_retained line 260