OAI/Combinatorics/KMedianRecovery/Recovery/Map.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MetricKMedianRecovery.PhaseMergeCompletion.Attains.map line 12
2. lemma OAI.MetricKMedianRecovery.PhaseMergeCompletion.Attains.insert_disabled line 26
3. lemma OAI.MetricKMedianRecovery.PhaseMergeCompletion.Attains.swap_free line 39
4. def OAI.MetricKMedianRecovery.PhaseLengthInterpolation.leafPhase line 70
5. lemma OAI.MetricKMedianRecovery.PhaseLengthInterpolation.leaf_boundary line 73
6. theorem OAI.MetricKMedianRecovery.PhaseLengthInterpolation.leaf_valid line 79
7. lemma OAI.MetricKMedianRecovery.PhaseLengthInterpolation.leaf_free_count line 102
8. theorem OAI.MetricKMedianRecovery.PhaseLengthInterpolation.leaf_attains line 115