OAI/Combinatorics/KMedianRecovery/Branching/CompletionBound.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MetricKMedianRecovery.RationalPhase.finish_events line 8
2. lemma OAI.MetricKMedianRecovery.RationalPhase.completion_events line 25
3. lemma OAI.MetricKMedianRecovery.FiniteLabelContinuation.select_card line 38
4. lemma OAI.MetricKMedianRecovery.FiniteLabelContinuation.complete_events line 42