Induced forest number

DefinitionInduced forest number#✓fully proved

For a simple graph \(G\) on a finite vertex set \(V\), the induced forest number \(a(G)\) is the maximum number of vertices of an induced forest in \(G\), that is, the maximum cardinality of a set \(S \subseteq V\) such that the subgraph of \(G\) induced on \(S\) is acyclic.

noncomputable def inducedForestNumber (G : SimpleGraph V) : Nat := by
  classical
  exact Finset.sup (Finset.univ.powerset (α := V))
    (fun (s : Finset V) => if (G.induce (↑s : Set V)).IsAcyclic then s.card else 0)

Sources

H. Jung, A 15/31 Counterexample Family to the Albertson--Berman Conjecture, arXiv:2608.17350v1, the definition of \(a(G)\).

Used by 3

Used byInduced forests are no larger than the induced forest number · The induced forest number is attained · The induced forest number is at most the number of vertices

TheoremInduced forests are no larger than the induced forest number#✓fully proved

Let \(G\) be a simple graph on a finite vertex set \(V\). For every set \(S \subseteq V\) such that the subgraph of \(G\) induced on \(S\) is acyclic, \(|S|\) is at most the induced forest number of \(G\).

theorem card_le_inducedForestNumber (G : SimpleGraph V) (s : Finset V)
    (h : (G.induce (↑s : Set V)).IsAcyclic) :
    s.card ≤ G.inducedForestNumber

Uses 1

Statement usesInduced forest number

TheoremThe induced forest number is at most the number of vertices#✓fully proved

For every simple graph \(G\) on a finite vertex set \(V\), the induced forest number of \(G\) is at most \(|V|\).

theorem inducedForestNumber_le_card (G : SimpleGraph V) :
    G.inducedForestNumber ≤ Fintype.card V

Uses 1

Statement usesInduced forest number

TheoremThe induced forest number is attained#✓fully proved

For every simple graph \(G\) on a finite vertex set \(V\), there is a set \(S \subseteq V\) such that the subgraph of \(G\) induced on \(S\) is acyclic and \(|S|\) equals the induced forest number of \(G\).

theorem exists_isAcyclic_card_eq_inducedForestNumber (G : SimpleGraph V) :
    ∃ s : Finset V, (G.induce (↑s : Set V)).IsAcyclic ∧ s.card = G.inducedForestNumber

Uses 1

Statement usesInduced forest number

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.