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

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Components after deleting the two common neighbours' endpoints.

  1. theorem OAI.CycleClique.Construction.deleted_component_neighbor_cover line 10

    Source documentation

    A neighbour of a vertex in a component after deleting y,z is either one of these two vertices or a neighbour in that component.

    theorem deleted_component_neighbor_cover {V : Type*} {H : SimpleGraph V} {y z : V}
    (C : (H.induce {v | v ≠ y ∧ v ≠ z}).ConnectedComponent)
    (u : C) {v : V} (h : H.Adj u.val.val v) :
    v = y ∨ v = z ∨ ∃ w : C, C.toSimpleGraph.Adj u w ∧ w.val.val = v := by
…
  2. theorem OAI.CycleClique.Construction.deleted_component_degree_loss line 23
  3. theorem OAI.CycleClique.Construction.deleted_component_min_degree line 51
  4. theorem OAI.CycleClique.Construction.deleted_component_cliqueNum_le line 61