OAI/Combinatorics/KMedianRecovery/Recovery/MergeRefine.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.PhaseMergeRefinement.Good line 12
  2. def OAI.MetricKMedianRecovery.PhaseMergeRefinement.Coincident line 15
  3. inductive OAI.MetricKMedianRecovery.PhaseMergeRefinement.Edit line 20
  4. def OAI.MetricKMedianRecovery.PhaseMergeRefinement.Adjacent line 27
  5. inductive OAI.MetricKMedianRecovery.PhaseMergeRefinement.Chain line 30
  6. lemma OAI.MetricKMedianRecovery.PhaseMergeRefinement.Chain.trans line 37
  7. lemma OAI.MetricKMedianRecovery.PhaseMergeRefinement.Chain.first_good line 44
  8. lemma OAI.MetricKMedianRecovery.PhaseMergeRefinement.Chain.last_good line 51
  9. lemma OAI.MetricKMedianRecovery.PhaseMergeRefinement.Chain.symm line 58
  10. lemma OAI.MetricKMedianRecovery.PhaseMergeRefinement.Good.mono_free line 66
  11. lemma OAI.MetricKMedianRecovery.PhaseMergeRefinement.cap_append line 72
  12. lemma OAI.MetricKMedianRecovery.PhaseMergeRefinement.entry_fresh line 85
  13. theorem OAI.MetricKMedianRecovery.PhaseMergeRefinement.suffix_chain line 96
  14. theorem OAI.MetricKMedianRecovery.PhaseMergeRefinement.remove_refinement line 112
  15. lemma OAI.MetricKMedianRecovery.PhaseMergeRefinement.Edit.mono_free line 159
  16. lemma OAI.MetricKMedianRecovery.PhaseMergeRefinement.Chain.mono_free line 166
  17. lemma OAI.MetricKMedianRecovery.PhaseMergeRefinement.good_of_one line 175
  18. theorem OAI.MetricKMedianRecovery.PhaseMergeRefinement.refine_walk line 180
  19. theorem OAI.MetricKMedianRecovery.PhaseMergeRefinement.regular_phase_chain line 225
  20. inductive OAI.MetricKMedianRecovery.CanonicalMergeRefinement.Jump line 250
  21. def OAI.MetricKMedianRecovery.CanonicalMergeRefinement.Jump.source line 256
  22. def OAI.MetricKMedianRecovery.CanonicalMergeRefinement.Jump.target line 261
  23. def OAI.MetricKMedianRecovery.CanonicalMergeRefinement.Jump.labels line 266
  24. instance OAI.MetricKMedianRecovery.CanonicalMergeRefinement.(instance at line 271) line 271
  25. def OAI.MetricKMedianRecovery.CanonicalMergeRefinement.cuts line 274
  26. lemma OAI.MetricKMedianRecovery.CanonicalMergeRefinement.mem_cuts line 279
  27. lemma OAI.MetricKMedianRecovery.CanonicalMergeRefinement.cuts_length line 299
  28. def OAI.MetricKMedianRecovery.CanonicalMergeRefinement.candidates line 304
  29. def OAI.MetricKMedianRecovery.CanonicalMergeRefinement.accepts line 309
  30. instance OAI.MetricKMedianRecovery.CanonicalMergeRefinement.(instance at line 312) line 312
  31. def OAI.MetricKMedianRecovery.CanonicalMergeRefinement.view line 315
  32. lemma OAI.MetricKMedianRecovery.CanonicalMergeRefinement.candidates_length line 319
  33. lemma OAI.MetricKMedianRecovery.CanonicalMergeRefinement.view_sound line 324
  34. lemma OAI.MetricKMedianRecovery.CanonicalMergeRefinement.view_exists line 329
  35. inductive OAI.MetricKMedianRecovery.CanonicalMergeRefinement.EPath line 359
  36. lemma OAI.MetricKMedianRecovery.CanonicalMergeRefinement.EPath.toChain line 367
  37. lemma OAI.MetricKMedianRecovery.CanonicalMergeRefinement.EPath.first_good line 374
  38. lemma OAI.MetricKMedianRecovery.CanonicalMergeRefinement.EPath.last_good line 378
  39. lemma OAI.MetricKMedianRecovery.CanonicalMergeRefinement.EPath.append line 382
  40. lemma OAI.MetricKMedianRecovery.CanonicalMergeRefinement.EPath.mono_free line 390
  41. def OAI.MetricKMedianRecovery.CanonicalMergeRefinement.growSuffix line 399
  42. lemma OAI.MetricKMedianRecovery.CanonicalMergeRefinement.growSuffix_length line 404
  43. theorem OAI.MetricKMedianRecovery.CanonicalMergeRefinement.growSuffix_spec line 409
  44. def OAI.MetricKMedianRecovery.CanonicalMergeRefinement.removeVertices line 427
  45. lemma OAI.MetricKMedianRecovery.CanonicalMergeRefinement.removeVertices_length line 431
  46. theorem OAI.MetricKMedianRecovery.CanonicalMergeRefinement.removeVertices_spec line 435
  47. def OAI.MetricKMedianRecovery.CanonicalMergeRefinement.Jump.expand line 474
  48. theorem OAI.MetricKMedianRecovery.CanonicalMergeRefinement.expand_spec line 479
  49. def OAI.MetricKMedianRecovery.CanonicalMergeRefinement.refinePath line 523
  50. theorem OAI.MetricKMedianRecovery.CanonicalMergeRefinement.refinePath_spec line 531
  51. def OAI.MetricKMedianRecovery.CanonicalMergeRefinement.regularChain line 560
  52. theorem OAI.MetricKMedianRecovery.CanonicalMergeRefinement.regularChain_spec line 564