CubicPathwidth.Alg.Proofs2.X3DegreeTransfer

Source file CubicPathwidth/Alg/Proofs2/X3DegreeTransfer.lean of the Lean project (how it is built).

import CubicPathwidth.Alg.Plan2

/-!
Stage 2 task X3: `DegreeTransfer`.

Let `S` be a relabelling of `G` by the injection `e`. Then `e` maps `S.neighborFinset i`
bijectively onto the neighbour list `G.nbrs (e i)`: every neighbour is a node, hence
`e j` for some `j`, and `S.Adj i j ↔ G.Adj (e i) (e j)`. The neighbour list has no
repeats (`WF`), so its length is the card of its `toFinset`.
-/

namespace CubicPathwidth.Alg

open Graph

/-- Degrees are preserved by a relabelling. -/
theorem degreeTransfer : DegreeTransfer := by
  classical
  unfold DegreeTransfer
  intro G m S e hG hrel i
  obtain ⟨hinj, hnodes, hadj⟩ := hrel
  rw [← SimpleGraph.card_neighborFinset_eq_degree, ← Finset.card_image_of_injective _ hinj]
  have himg : (S.neighborFinset i).image e = (G.nbrs (e i)).toFinset := by
    ext x
    simp only [Finset.mem_image, SimpleGraph.mem_neighborFinset, List.mem_toFinset]
    constructor
    · rintro ⟨j, hj, rfl⟩
      exact (hadj i j).1 hj
    · intro hx
      obtain ⟨j, rfl⟩ := (hnodes x).1 (hG.nbrs_sub _ _ hx)
      exact ⟨j, (hadj i j).2 hx, rfl⟩
  rw [himg, List.toFinset_card_of_nodup (hG.nbrs_nodup _)]
  rfl

#print axioms CubicPathwidth.Alg.degreeTransfer

end CubicPathwidth.Alg
Back to top