OAI/Combinatorics/KMedianRecovery/Branching/PopulationBridge.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MetricKMedianRecovery.BitMachine.RationalMin.fold_lower_real line 8
2. lemma OAI.MetricKMedianRecovery.BitMachine.RationalMin.minimum_lower_real line 19
3. def OAI.MetricKMedianRecovery.BitMachine.BinaryPopulation.distanceList line 30
4. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryPopulation.filter_count_cast line 32
5. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryPopulation.candidate_cast line 41
6. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryPopulation.distanceList_nonempty line 46
7. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryPopulation.radiusQ_cast line 52