def SimpleGraph.IsPathCover {α : Type u_1} [Fintype α] [DecidableEq α] (G : SimpleGraph α) (P : Finset (Finset α)) : Prop

A family of paths covering all vertices without overlaps.

Equations

• G.IsPathCover P = ((∀ s1 ∈ P, ∀ s2 ∈ P, s1 ≠ s2 → Disjoint s1 s2) ∧ Finset.univ ⊆ P.biUnion id ∧ ∀ s ∈ P, ∃ (u : α) (v : α) (p : G.Walk u v), p.IsPath ∧ s = p.support.toFinset)

noncomputable def SimpleGraph.pathCoverNumber {α : Type u_1} [Fintype α] [DecidableEq α] (G : SimpleGraph α) : ℕ

Minimum size of a path cover of G.

Equations

• G.pathCoverNumber = sInf {k : ℕ | ∃ (P : Finset (Finset α)), P.card = k ∧ G.IsPathCover P}