OAI/Combinatorics/RamseyFive/Geometry/ReverseAfterCapture.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.SharpRamseyFive.ProjectiveIncidence.reverse_after_captureline 15 - lemma
OAI.SharpRamseyFive.ProjectiveIncidence.source_product_to_capline 46 - lemma
OAI.SharpRamseyFive.ProjectiveIncidence.reverse_capture_costline 57