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

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Realizing a component of the two-vertex deletion as ambient vertices.

  1. def OAI.CycleClique.Construction.deletedComponentEmbedding line 8
  2. def OAI.CycleClique.Construction.componentVertices line 12
  3. theorem OAI.CycleClique.Construction.mem_componentVertices line 18
  4. theorem OAI.CycleClique.Construction.deleted_not_componentVertices line 32
  5. theorem OAI.CycleClique.Construction.componentVertices_neighbor_cover line 44
  6. theorem OAI.CycleClique.Construction.componentVertices_connected line 55
  7. theorem OAI.CycleClique.Construction.induced_degree_loss_pair line 72

    Source documentation

    Restriction to a vertex set closed under all other neighbours loses at most the two deleted neighbours.

    theorem induced_degree_loss_pair {V : Type*} [Fintype V]
    {H : SimpleGraph V} {U : Finset V} {y z : V}
    (hcover : ∀ u ∈ U, ∀ v, H.Adj u v → v ∈ U ∨ v = y ∨ v = z)
    (u : (U : Set V)) :
    (H.neighborSet u.val).ncard ≤ ((H.induce (U : Set V)).neighborSet u).ncard + 2 := by
…