CubicPathwidth.Alg.Proofs.G1WFBasics

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

import CubicPathwidth.Alg.Spec

/-!
Task G1: `WFBasics`, obtained directly from the fields of `Graph.WF`.
-/

namespace CubicPathwidth.Alg

namespace G1

/-- Adjacency is symmetric and both ends are nodes, as a plain statement about `nbrs`. -/
theorem adj_facts {G : Graph} (hG : G.WF) {u v : Nat} (h : v ∈ G.nbrs u) :
    u ∈ G.nodes ∧ v ∈ G.nodes ∧ u ∈ G.nbrs v ∧ u ≠ v := by
  refine ⟨?_, hG.nbrs_sub u v h, hG.symm u v h, ?_⟩
  · exact hG.nbrs_sub v u (hG.symm u v h)
  · intro huv
    subst huv
    exact hG.loopless u h

end G1

theorem wfBasics : WFBasics := by
  intro G hG u v h
  obtain ⟨h1, h2, h3, h4⟩ := G1.adj_facts hG h
  exact ⟨h1, h2, h3, h4⟩

#print axioms CubicPathwidth.Alg.wfBasics

end CubicPathwidth.Alg
Back to top