OAI/Combinatorics/RamseyFive/Geometry/CardFilterContainment.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SharpRamseyFive.RichPlaneGeometry.card_filter_containment_le line 12
2. lemma OAI.SharpRamseyFive.RichPlaneGeometry.card_filter_finrank_le_two line 24
3. lemma OAI.SharpRamseyFive.RichPlaneGeometry.card_filter_finrank_le_one line 32
4. lemma OAI.SharpRamseyFive.RichPlaneGeometry.finrank_inf_lt_of_not_le line 41
5. lemma OAI.SharpRamseyFive.RichPlaneGeometry.plane_noncontaining_flat_cap line 48
6. lemma OAI.SharpRamseyFive.RichPlaneGeometry.line_noncontaining_flat_cap line 55
7. lemma OAI.SharpRamseyFive.RichPlaneGeometry.card_hyperplane_family line 62
8. lemma OAI.SharpRamseyFive.RichPlaneGeometry.card_hyperplanes_inside line 76
9. lemma OAI.SharpRamseyFive.HyperplaneOverlap.hyperplane_intersection_rank line 98
10. lemma OAI.SharpRamseyFive.HyperplaneOverlap.card_hyperplanes_containing line 110
11. lemma OAI.SharpRamseyFive.HyperplaneOverlap.pair_count_by_intersection line 136
12. lemma OAI.SharpRamseyFive.HyperplaneOverlap.neighbor_count_by_intersection line 157
13. lemma OAI.SharpRamseyFive.HyperplaneOverlap.pair_count_by_contained_witness line 173
14. lemma OAI.SharpRamseyFive.HyperplaneOverlap.neighbor_count_by_contained_witness line 196
15. lemma OAI.SharpRamseyFive.HyperplaneOverlap.rich_radial_count line 213
16. lemma OAI.SharpRamseyFive.HyperplaneOverlap.rich_radial_strength_count line 224