OAI/Combinatorics/KMedianRecovery/Recovery/Coupled.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- structure
OAI.MetricKMedianRecovery.PhaseCoupledMerge.Coupledline 12 - lemma
OAI.MetricKMedianRecovery.PhaseCoupledMerge.disjoint_mapline 38 - lemma
OAI.MetricKMedianRecovery.PhaseCoupledMerge.Coupled.zero_falseline 46 - def
OAI.MetricKMedianRecovery.PhaseCoupledMerge.sameline 58 - theorem
OAI.MetricKMedianRecovery.PhaseCoupledMerge.advanceline 88