OAI/Combinatorics/RamseyFive/Geometry/ReverseAfterCapture.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SharpRamseyFive.ProjectiveIncidence.reverse_after_capture line 15
  2. lemma OAI.SharpRamseyFive.ProjectiveIncidence.source_product_to_cap line 46
  3. lemma OAI.SharpRamseyFive.ProjectiveIncidence.reverse_capture_cost line 57