OAI/Combinatorics/RamseyFive/Geometry/FlatSection.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SharpRamseyFive.ProjectiveRestriction.flatEmbedding line 15
  2. def OAI.SharpRamseyFive.ProjectiveRestriction.flatSection line 19
  3. lemma OAI.SharpRamseyFive.ProjectiveRestriction.section_mono line 22
  4. lemma OAI.SharpRamseyFive.ProjectiveRestriction.range_flatEmbedding line 27
  5. lemma OAI.SharpRamseyFive.ProjectiveRestriction.section_map line 45
  6. lemma OAI.SharpRamseyFive.ProjectiveRestriction.section_card line 56
  7. lemma OAI.SharpRamseyFive.ProjectiveRestriction.section_degree_sum line 60
  8. lemma OAI.SharpRamseyFive.ProjectiveRestriction.incidences_mono_left line 71
  9. lemma OAI.SharpRamseyFive.ProjectiveRestriction.section_density line 77
  10. lemma OAI.SharpRamseyFive.ProjectiveRestriction.section_decoder line 89
  11. theorem OAI.SharpRamseyFive.ProjectiveRestriction.original_large_cell line 114