OAI/Combinatorics/KMedian/Sparse/SparseSupplierSupport.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MetricKMedian.SparseIntegerLaw.bindIndexed_contains line 15
2. theorem OAI.MetricKMedian.SparsePrepared.contains_encoded line 30
3. def OAI.MetricKMedian.Preparation.RationalSuppliers.physicalIndex line 60
4. def OAI.MetricKMedian.Preparation.RationalSuppliers.original line 63
5. def OAI.MetricKMedian.Preparation.RationalSuppliers.counts line 65
6. theorem OAI.MetricKMedian.Preparation.RationalSuppliers.coupled_support line 71