OAI/Combinatorics/RamseyFive/Marking/WindowLevels.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.SharpRamseyFive.Marking.ReciprocalWindows line 18
  2. def OAI.SharpRamseyFive.Marking.ReciprocalWindows.firstReference line 32
  3. def OAI.SharpRamseyFive.Marking.ReciprocalWindows.secondReference line 36
  4. def OAI.SharpRamseyFive.Marking.ReciprocalWindows.firstSupport line 40
  5. def OAI.SharpRamseyFive.Marking.ReciprocalWindows.secondSupport line 42
  6. lemma OAI.SharpRamseyFive.Marking.ReciprocalWindows.first_nonempty line 46
  7. lemma OAI.SharpRamseyFive.Marking.ReciprocalWindows.second_nonempty line 49
  8. lemma OAI.SharpRamseyFive.Marking.ReciprocalWindows.first_domination line 52
  9. lemma OAI.SharpRamseyFive.Marking.ReciprocalWindows.second_domination line 58
  10. lemma OAI.SharpRamseyFive.Marking.ReciprocalWindows.support_product line 65
  11. lemma OAI.SharpRamseyFive.Marking.ReciprocalWindows.reference_sparse line 80
  12. lemma OAI.SharpRamseyFive.Marking.ReciprocalWindows.target_right_sparse line 90
  13. lemma OAI.SharpRamseyFive.Marking.ReciprocalWindows.target_left_sparse line 102
  14. theorem OAI.SharpRamseyFive.Marking.reciprocal_windows_exist line 114