OAI/Combinatorics/KMedian/Probability/ProbabilitySupport.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MetricKMedian.FiniteLaw.expect_mono_support line 10
2. theorem OAI.MetricKMedian.FiniteLaw.expect_congr_support line 19
3. theorem OAI.MetricKMedian.FiniteLaw.prob_zero_support line 25
4. theorem OAI.MetricKMedian.FiniteLaw.prob_compl line 37
5. theorem OAI.MetricKMedian.FiniteLaw.prob_one_support line 44
6. theorem OAI.MetricKMedian.FiniteLaw.support_product line 52