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

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Starting the coloured-path argument

The first step of manuscript Lemma clq:coloured-path is proved by walk induction: preservation of colour across two steps, together with one monochromatic edge, makes the colour constant on its component.

  1. theorem OAI.CycleClique.Construction.color_eq_of_walk line 16
  2. theorem OAI.CycleClique.Construction.differently_colored_common_neighbors line 27

    Source documentation

    In a connected nonbipartite graph, any nonconstant two-colouring has differently coloured vertices sharing a neighbour.

    theorem differently_colored_common_neighbors {V : Type*} {G : SimpleGraph V}
    (hconnected : G.Connected) (hnonbipartite : ¬ G.IsBipartite)
    (χ : V → Fin 2) (hnonconstant : ∃ u v, χ u ≠ χ v) :
    ∃ x y z, G.Adj x y ∧ G.Adj x z ∧ χ y ≠ χ z := by
…