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

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The application-sized Chvátal–Erdős theorem: alpha at most two.

  1. theorem OAI.CycleClique.Construction.ce_exists_longest_cycle line 10
  2. theorem OAI.CycleClique.Construction.ceAlphaTwo_proved line 41

    Source documentation

    Chvátal–Erdős (1972), Theorem 1, in the precise specialization used by the conditional Ramsey development.

    theorem ceAlphaTwo_proved : CEAlphaTwo := by
…

    Mentions: OAI.CycleClique.Construction.CEAlphaTwo