OAI/Combinatorics/KMedian/Sparse/SparseRealLaw.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedian.RationalLaw.real line 11
2. theorem OAI.MetricKMedian.RationalLaw.real_expect line 16
3. def OAI.MetricKMedian.SparseIntegerLaw.realIndex line 25
4. theorem OAI.MetricKMedian.SparseIntegerLaw.realIndex_expect line 28
5. def OAI.MetricKMedian.SparseIntegerLaw.real line 32
6. theorem OAI.MetricKMedian.SparseIntegerLaw.real_expect line 35
7. theorem OAI.MetricKMedian.SparseIntegerLaw.real_property line 39