OAI/Combinatorics/RamseyFive/Geometry/RichHyperplaneVariance.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SharpRamseyFive.RichPlaneGeometry.rich_hyperplane_variance line 15
2. theorem OAI.SharpRamseyFive.RichPlaneGeometry.rich_subspaces_variance line 48
3. def OAI.SharpRamseyFive.RichPlaneGeometry.pointsInSubspace line 75
4. lemma OAI.SharpRamseyFive.RichPlaneGeometry.card_pointsInSubspace line 79
5. lemma OAI.SharpRamseyFive.RichPlaneGeometry.mem_pointsInSubspace line 83
6. lemma OAI.SharpRamseyFive.RichPlaneGeometry.subspacePointsEquiv_submodule line 87
7. lemma OAI.SharpRamseyFive.RichPlaneGeometry.card_pointsInSubspace_filter line 97
8. lemma OAI.SharpRamseyFive.RichPlaneGeometry.comap_subtype_finrank line 120
9. lemma OAI.SharpRamseyFive.RichPlaneGeometry.comap_subtype_injOn line 124
10. theorem OAI.SharpRamseyFive.RichPlaneGeometry.rich_hyperplanes_inside_subspace line 132
11. theorem OAI.SharpRamseyFive.RichPlaneGeometry.rich_planes_inside_hyperplane line 160