Lax Lean Archive

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

Vertex-cover number

Lax825442.VertexCover · concepts/Lax825442/VertexCover.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

    The vertex-cover number is the minimum size of a set meeting every edge. This natural-valued interface refers to mathlib’s vertex-cover number; it is finite on finite graphs. Mathlib's SimpleGraph.vertexCoverNumnetopoffiniteSimpleGraph.vertexCoverNum_ne_top_of_finite ensures that conversion to a natural number loses no information in this domain.

    Concept map
    1 concept
    100%
    DefinitionThis concept

    Lean source view on GitHub

    1import Mathlib.Combinatorics.SimpleGraph.VertexCover
    2
    3/-!
    4---
    5title: Vertex-cover number
    6type: definition
    7---
    8The vertex-cover number is the minimum size of a set meeting every edge. This
    9natural-valued interface refers to mathlib’s vertex-cover number; it is finite
    10on finite graphs.
    11Mathlib's `SimpleGraph.vertexCoverNum_ne_top_of_finite` ensures that conversion
    12to a natural number loses no information in this domain.
    13-/
    14
    15namespace Lax825442.VertexCover
    16
    17/-- The natural-valued vertex-cover number of a finite graph. -/
    18noncomputable def vertexCover {V : Type} [Fintype V] [DecidableEq V]
    19 (G : SimpleGraph V) : ℕ :=
    20 G.vertexCoverNum.toNat
    21
    22end Lax825442.VertexCover
    23
    24
    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…