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

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The complete ground set and representative finset of an optimal system.

  1. def OAI.CycleClique.Construction.ExpandedPathSystem.ground line 14
  2. def OAI.CycleClique.Construction.ExpandedPathSystem.representativeFinset line 16
  3. theorem OAI.CycleClique.Construction.ExpandedPathSystem.ground_card line 19
  4. theorem OAI.CycleClique.Construction.ExpandedPathSystem.representativeFinset_card line 26
  5. theorem OAI.CycleClique.Construction.ExpandedPathSystem.representativeFinset_subset_ground line 31
  6. theorem OAI.CycleClique.Construction.ExpandedPathSystem.IsOptimal.ground_card_le line 39
  7. theorem OAI.CycleClique.Construction.ExpandedPathSystem.IsOptimal.representativeFinset_one_exclusion line 45