OAI/Combinatorics/RamseyFive/Geometry/MemPairRank.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SharpRamseyFive.SpanRank.mem_pair_iff_rank line 17
2. lemma OAI.SharpRamseyFive.AffineRealization.span_pair_eq_line line 50
3. theorem OAI.SharpRamseyFive.AffineRealization.line_incidence_of_ranks line 62
4. theorem OAI.SharpRamseyFive.AffineRealization.distinct_lines_of_ranks line 85
5. theorem OAI.SharpRamseyFive.AffineRealization.line_count_of_ranks line 118
6. theorem OAI.SharpRamseyFive.AffineRealization.exists_line_indices line 143
7. theorem OAI.SharpRamseyFive.AffineRealization.projective_line_card_le_sq line 154