Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

Arboricity

Lax825442.Arboricity · concepts/Lax825442/Arboricity.lean · lax-825442

definition

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Definition

    Arboricity is the minimum number of forests partitioning the edge set. An edgeless graph has value zero.

    Concept map
    1 concept
    100%
    DefinitionThis concept

    Lean source view on GitHub

    1import Mathlib.Combinatorics.SimpleGraph.Acyclic
    2import Mathlib.Combinatorics.SimpleGraph.Finite
    3import Mathlib.Order.Lattice.Nat
    4
    5/-!
    6---
    7title: Arboricity
    8type: definition
    9---
    10Arboricity is the minimum number of forests partitioning the edge set. An
    11edgeless graph has value zero.
    12-/
    13
    14namespace Lax825442.Arboricity
    15
    16/-- An assignment of graph edges to `k` classes, each inducing a forest. -/
    17def HasArboricityAtMost {V : Type} [Fintype V] [DecidableEq V]
    18 (G : SimpleGraph V) (k : ℕ) : Prop :=
    19 ∃ color : G.edgeSet → Fin k,
    20 (∀ i : Fin k,
    21 (G.deleteEdges {e : Sym2 V | ∃ h : e ∈ G.edgeSet,
    22 color ⟨e, h⟩ ≠ i}).IsAcyclic)
    23
    24/-- The minimum number of forests partitioning the edges. -/
    25noncomputable def arboricity {V : Type} [Fintype V] [DecidableEq V]
    26 (G : SimpleGraph V) : ℕ :=
    27 sInf {k | HasArboricityAtMost G k}
    28
    29end Lax825442.Arboricity
    30
    Builds on

    none

    Used by

    none

    From Mathlib

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…