OAI/Combinatorics/EuclideanRamsey/DerivedFractions.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.EuclideanRamsey.Derived line 30
  2. instance OAI.EuclideanRamsey.derived_normal line 33
  3. lemma OAI.EuclideanRamsey.derived_le line 37
  4. def OAI.EuclideanRamsey.PairCoverage line 42
  5. def OAI.EuclideanRamsey.restrictionHom line 45
  6. lemma OAI.EuclideanRamsey.restrict_diagonal line 50
  7. lemma OAI.EuclideanRamsey.restrict_pairInverse line 54
  8. lemma OAI.EuclideanRamsey.restrict_pairCoverage line 59
  9. lemma OAI.EuclideanRamsey.lift_restricted_fraction line 66
  10. lemma OAI.EuclideanRamsey.pair_commutator_fraction line 75
  11. lemma OAI.EuclideanRamsey.fraction_card_le_two line 96
  12. theorem OAI.EuclideanRamsey.derived_subset_single line 124
  13. def OAI.EuclideanRamsey.freeAugmentation line 182
  14. def OAI.EuclideanRamsey.AugKernel line 184
  15. instance OAI.EuclideanRamsey.(instance at line 185) line 185
  16. lemma OAI.EuclideanRamsey.letter_difference_mem line 186
  17. lemma OAI.EuclideanRamsey.augmentation_kernel_le line 190