Lax Lean Archive

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

Maximum matching number

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

    A matching is a set of edges with no shared endpoints. The maximum matching number of a finite simple graph is the largest number of edges in a matching. The empty graph has value zero. The definition uses mathlib's subgraph matching predicate and counts edges, rather than matched vertices.

    Concept map
    1 concept
    100%
    DefinitionThis concept

    Lean source view on GitHub

    1import Mathlib.Combinatorics.SimpleGraph.Matching
    2import Mathlib.Order.Lattice.Nat
    3import Mathlib.Data.Set.Card
    4
    5/-!
    6---
    7title: Maximum matching number
    8type: definition
    9---
    10A matching is a set of edges with no shared endpoints. The maximum matching
    11number of a finite simple graph is the largest number of edges in a matching.
    12The empty graph has value zero. The definition uses mathlib's subgraph
    13matching predicate and counts edges, rather than matched vertices.
    14-/
    15
    16namespace Lax825442.MaximumMatching
    17
    18/-- The maximum number of edges in a matching. -/
    19noncomputable def maximumMatching {V : Type} [Fintype V] [DecidableEq V]
    20 (G : SimpleGraph V) : ℕ :=
    21 sSup {n : ℕ | ∃ M : G.Subgraph, M.IsMatching ∧ (M.edgeSet.ncard = n)}
    22
    23end Lax825442.MaximumMatching
    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…