OAI/Combinatorics/KMedian/Programs/NearestMaskProgram.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedian.Preparation.RationalNearest.MaskProgram.erase line 15
2. def OAI.MetricKMedian.Preparation.RationalNearest.MaskProgram.insert line 16
3. theorem OAI.MetricKMedian.Preparation.RationalNearest.MaskProgram.erase_poly line 17
4. theorem OAI.MetricKMedian.Preparation.RationalNearest.MaskProgram.insert_poly line 21
5. theorem OAI.MetricKMedian.Preparation.RationalNearest.MaskProgram.erase_view line 22
6. theorem OAI.MetricKMedian.Preparation.RationalNearest.MaskProgram.insert_view line 30
7. def OAI.MetricKMedian.Preparation.RationalNearest.MaskProgram.raw line 38
8. theorem OAI.MetricKMedian.Preparation.RationalNearest.MaskProgram.raw_poly line 44
9. theorem OAI.MetricKMedian.Preparation.RationalNearest.MaskProgram.raw_view line 52