OAI/Geometry/PinnedDistances/ExtremalFractions.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.WeakPinned.richPairs_subset_offDiag line 29
  2. lemma OAI.WeakPinned.richPairs_card_le line 34
  3. lemma OAI.WeakPinned.pairFraction_nonneg line 39
  4. lemma OAI.WeakPinned.pairFraction_le_one line 45
  5. lemma OAI.WeakPinned.fraction_values_nonempty line 57
  6. lemma OAI.WeakPinned.fraction_values_bddAbove line 62
  7. lemma OAI.WeakPinned.fraction_le_F line 68
  8. lemma OAI.WeakPinned.F_nonneg line 72
  9. lemma OAI.WeakPinned.F_le_one line 79
  10. lemma OAI.WeakPinned.F_attained line 85
  11. lemma OAI.WeakPinned.k_lt_card line 117
  12. lemma OAI.WeakPinned.richPairs_antitone line 122
  13. lemma OAI.WeakPinned.fraction_antitone line 130
  14. lemma OAI.WeakPinned.F_antitone line 138
  15. lemma OAI.WeakPinned.F_eq_zero_of_one_le line 149