OAI/Combinatorics/RamseyFive/Geometry/ProjectiveEquiv.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpRamseyFive.ProjectiveIncidence.projectiveEquiv line 14
2. lemma OAI.SharpRamseyFive.ProjectiveIncidence.incident_mk_right line 24
3. lemma OAI.SharpRamseyFive.ProjectiveIncidence.incident_eval line 33
4. def OAI.SharpRamseyFive.ProjectiveIncidence.weightOnPencil line 42
5. lemma OAI.SharpRamseyFive.ProjectiveIncidence.weightOnPencil_eq line 46
6. theorem OAI.SharpRamseyFive.ProjectiveIncidence.pencil_variance line 53