OAI/Combinatorics/RamseyFive/Geometry/OriginalReadiness.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SharpRamseyFive.ProjectiveIncidence.not_original_ready_iff line 17
  2. theorem OAI.SharpRamseyFive.ProjectiveIncidence.original_not_ready_mass line 25
  3. theorem OAI.SharpRamseyFive.ProjectiveIncidence.oriented_level_not_ready line 68