OAI/Combinatorics/KMedianRecovery/Recovery/Height.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.RationalHeight.Height line 8
  2. lemma OAI.MetricKMedianRecovery.RationalHeight.Height.mono line 10
  3. lemma OAI.MetricKMedianRecovery.RationalHeight.zero line 13
  4. lemma OAI.MetricKMedianRecovery.RationalHeight.of_fraction line 18
  5. lemma OAI.MetricKMedianRecovery.RationalHeight.natCast line 32
  6. lemma OAI.MetricKMedianRecovery.RationalHeight.Height.neg line 37
  7. lemma OAI.MetricKMedianRecovery.RationalHeight.Height.add line 40
  8. lemma OAI.MetricKMedianRecovery.RationalHeight.Height.sub line 62
  9. lemma OAI.MetricKMedianRecovery.RationalHeight.Height.mul line 67
  10. lemma OAI.MetricKMedianRecovery.RationalHeight.Height.inv line 81
  11. lemma OAI.MetricKMedianRecovery.RationalHeight.Height.div line 91
  12. lemma OAI.MetricKMedianRecovery.RationalHeight.Height.pow line 96
  13. lemma OAI.MetricKMedianRecovery.RationalHeight.sum line 103
  14. lemma OAI.MetricKMedianRecovery.RationalHeight.sqrtFraction line 115