OAI/Combinatorics/Ramsey/CycleClique/Construction/CertifiedRamseyReduction.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Mathematical assembly for a fixed cycle parameter, once its concrete finite certificate coverage has been proved.

  1. def OAI.CycleClique.Construction.CertificateCoverageAt line 14
  2. theorem OAI.CycleClique.Construction.no_expanded_counterexample_of_coverage line 18
  3. theorem OAI.CycleClique.Construction.cycle_clique_upper_of_coverage line 38
  4. theorem OAI.CycleClique.Construction.isRamseyNumber_of_certificate_coverage line 45