OAI/Combinatorics/IndependentSets/Geometry/RationalLaw.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.LargeIndependentSets.RationalLaw line 8
  2. def OAI.LargeIndependentSets.RationalLaw.denominator line 16
  3. def OAI.LargeIndependentSets.RationalLaw.copies line 18
  4. lemma OAI.LargeIndependentSets.RationalLaw.denominator_pos line 21
  5. lemma OAI.LargeIndependentSets.RationalLaw.denominator_dvd line 25
  6. lemma OAI.LargeIndependentSets.RationalLaw.copies_eq line 28
  7. lemma OAI.LargeIndependentSets.RationalLaw.total_copies line 45
  8. abbrev OAI.LargeIndependentSets.RationalLaw.Expanded line 51
  9. lemma OAI.LargeIndependentSets.RationalLaw.card_expanded line 53
  10. instance OAI.LargeIndependentSets.RationalLaw.expandedNonempty line 56
  11. lemma OAI.LargeIndependentSets.RationalLaw.copies_real line 59
  12. theorem OAI.LargeIndependentSets.RationalLaw.expect_expanded line 63
  13. abbrev OAI.LargeIndependentSets.RationalLaw.Vertices line 71
  14. lemma OAI.LargeIndependentSets.RationalLaw.card_vertices line 73
  15. lemma OAI.LargeIndependentSets.RationalLaw.expect_vertices line 77
  16. theorem OAI.LargeIndependentSets.density_le_location_square line 87
  17. theorem OAI.LargeIndependentSets.density_from_good_fibers line 98