OAI/Combinatorics/KMedian/Programs/FinsetMaskProgram.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.MetricKMedian.MaskProgram.get line 15
2. theorem OAI.MetricKMedian.MaskProgram.get_view line 16
3. def OAI.MetricKMedian.MaskProgram.intersect line 19
4. theorem OAI.MetricKMedian.MaskProgram.intersect_poly line 20
5. theorem OAI.MetricKMedian.MaskProgram.intersect_view line 25
6. def OAI.MetricKMedian.MaskProgram.selectedValues line 35
7. def OAI.MetricKMedian.MaskProgram.nearest line 37
8. theorem OAI.MetricKMedian.MaskProgram.selectedValues_poly line 39
9. theorem OAI.MetricKMedian.MaskProgram.nearest_poly line 44
10. theorem OAI.MetricKMedian.MaskProgram.selectedValues_mem line 48
11. theorem OAI.MetricKMedian.MaskProgram.nearest_view line 61