OAI/Combinatorics/KMedianRecovery/Sampling/ProbabilityCompEquiv.lean
2 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.MetricKMedianRecovery.FiniteSampling.probability_comp_equivline 7 - lemma
OAI.MetricKMedianRecovery.FiniteSampling.probability_ignore_middleline 12