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

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Normalizing a raw orientation preserves its ground, amount, optimality, and every representative, including its isolated clique vertices.

  1. theorem OAI.CycleClique.Construction.RawPathSystem.normalize_ground line 15
  2. theorem OAI.CycleClique.Construction.RawPathSystem.normalize_representative_mem line 26
  3. theorem OAI.CycleClique.Construction.ExpandedPathSystem.IsOptimal.of_amount_count line 64