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

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A short representative replacement cannot absorb any old assigned path. Consequently its two targets start two different oriented chains.

  1. theorem OAI.CycleClique.Construction.ExpandedPathSystem.mul_length_le_sum line 16
  2. theorem OAI.CycleClique.Construction.ExpandedPathSystem.IsOptimal.terminal_different_chain_starts line 26
  3. theorem OAI.CycleClique.Construction.ExpandedPathSystem.IsOptimal.terminal_same_chain_exclusion line 84