OAI/Combinatorics/KMedian/Reduction/CompletionMaskProgram.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedian.Completion.Rational.MaskOperations.integralRaw line 17
  2. theorem OAI.MetricKMedian.Completion.Rational.MaskOperations.integralRaw_poly line 19
  3. theorem OAI.MetricKMedian.Completion.Rational.MaskOperations.any_ofFn line 26
  4. theorem OAI.MetricKMedian.Completion.Rational.MaskOperations.integralRaw_view line 32
  5. def OAI.MetricKMedian.Completion.Rational.MaskOperations.uncoveredRaw line 66
  6. theorem OAI.MetricKMedian.Completion.Rational.MaskOperations.uncoveredRaw_poly line 69
  7. theorem OAI.MetricKMedian.Completion.Rational.MaskOperations.uncoveredRaw_view line 76
  8. def OAI.MetricKMedian.Completion.Rational.MaskOperations.firstCopy line 99
  9. theorem OAI.MetricKMedian.Completion.Rational.MaskOperations.firstCopy_poly line 100
  10. theorem OAI.MetricKMedian.Completion.Rational.MaskOperations.firstCopy_view line 101
  11. theorem OAI.MetricKMedian.Completion.Rational.MaskOperations.packing_map line 124