Lax Lean Archive

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

Matchings, the Matching Number, and Saturation

Lax117284.BipartiteMatching · concepts/Lax117284/BipartiteMatching.lean · lax-117284

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

    A matching of a graph is a set of edges no two of which share a vertex; the matching number is the largest number of edges in a matching; a matching saturates a set of vertices when it covers every one of them, and it is perfect when it covers every vertex of the graph.

    Concept map
    1 concept; 3 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Lean source view on GitHub

    1import Mathlib.Combinatorics.SimpleGraph.Matching
    2import Mathlib.Data.Set.Card
    3
    4/-!
    5---
    6title: Matchings, the Matching Number, and Saturation
    7type: definition
    8---
    9A matching of a graph is a set of edges no two of which share a vertex; the matching number is
    10the largest number of edges in a matching; a matching saturates a set of vertices when it covers
    11every one of them, and it is perfect when it covers every vertex of the graph.
    12
    13# Formalization Notes
    14
    15Matchings are Mathlib's: a subgraph `M` of `G` is a matching, `M.IsMatching`, when every vertex
    16of `M` has exactly one neighbour in `M`; its edges are `M.edgeSet`. Perfect matchings are
    17Mathlib's `IsPerfectMatching`. Only the size, the matching number, saturation and maximality are
    18named here.
    19
    20The matching number is the supremum of the sizes of the matchings. For a finite graph the set of
    21sizes is bounded by the number of edges and contains `0`, so the supremum is a maximum, attained
    22by some matching; a maximum matching is one that attains it.
    23-/
    24
    25namespace Lax117284.BipartiteMatching
    26
    27variable {V : Type*} (G : SimpleGraph V)
    28
    29/-- The size of a subgraph: the number of its edges. -/
    30noncomputable def size (M : G.Subgraph) : ℕ := M.edgeSet.ncard
    31
    32/-- **The matching number**: the largest size of a matching. -/
    33noncomputable def matchingNumber : ℕ :=
    34 sSup {k | ∃ M : G.Subgraph, M.IsMatching ∧ size G M = k}
    35
    36/-- **A maximum matching**: a matching no matching outnumbers. -/
    37def IsMaximumMatching (M : G.Subgraph) : Prop :=
    38 M.IsMatching ∧ ∀ M' : G.Subgraph, M'.IsMatching → size G M' ≤ size G M
    39
    40/-- **A subgraph saturates a set of vertices** when it contains every one of them. -/
    41def Saturates (M : G.Subgraph) (S : Set V) : Prop := S ⊆ M.verts
    42
    43end Lax117284.BipartiteMatching
    44
    Formalization Notes

    Matchings are Mathlib's: a subgraph MM of GG is a matching, M.IsMatchingM.IsMatching, when every vertex of MM has exactly one neighbour in MM; its edges are M.edgeSetM.edgeSet. Perfect matchings are Mathlib's IsPerfectMatchingIsPerfectMatching. Only the size, the matching number, saturation and maximality are named here.

    The matching number is the supremum of the sizes of the matchings. For a finite graph the set of sizes is bounded by the number of edges and contains 00, so the supremum is a maximum, attained by some matching; a maximum matching is one that attains it.

    Builds on

    none

    Used by
    From Mathlib

    Discussion

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

    Loading discussion…