PathJoining.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Joining disjoint paths through a clique

The expansions of the chains of a path system are disjoint simple paths with endpoints in the clique. Joining these paths, including any selected singleton clique vertices, gives the exact cycle used in path:interval.

theorem OAI.CycleClique.Construction.chain_of_pairwise line 17
Distinct definitions of this name: OAI/Combinatorics/Ramsey/CycleClique/Construction/CliqueTraversal.lean:24 (different declaration text). Qualify references as OAI.CycleClique.Construction.chain_of_pairwise@path.

theorem OAI.CycleClique.Construction.hasCycle_of_disjoint_clique_paths line 26

Source documentation

Disjoint simple paths whose endpoints lie in a common clique can be closed into a cycle through exactly all their vertices.

theorem hasCycle_of_disjoint_clique_paths {V : Type*} {G : SimpleGraph V}
    {Q : Set V} (hQ : G.IsClique Q) (L : List (List V))
    (hnonempty : ∀ l ∈ L, l ≠ [])
    (hpaths : ∀ l ∈ L, l.Nodup ∧ l.IsChain G.Adj)
    (hdisjoint : L.Pairwise List.Disjoint)
    (hendpoints : ∀ l ∈ L,
      (∀ v ∈ l.head?, v ∈ Q) ∧ (∀ v ∈ l.getLast?, v ∈ Q))
    (hlen : 3 ≤ L.flatten.length) : HasCycle G L.flatten.length := by
…

Mentions: OAI.CycleClique.Construction.HasCycle