Connected matchings

Lax342547.ConnectedMatching · concepts/Lax342547/ConnectedMatching.lean · lax-342547

definition

Loading review…

A connected matching is a matching whose distinct edges are joined by an edge. Its maximum size is the connected-matching number $\mathrm{cm}(G)$ .

Concept map

1 concept

100%

DefinitionThis conceptDescendants are omitted for concepts with more than 10 descendants.

Show types on hover

1	/-
2	Adapted from OpenAI, openai/math, commit
3	adc7f1241b42e322a6451854ab7e4b4c146bf78a (Apache-2.0).
4	Changes: Lax package separation, namespaces, explicit variables, and archive annotations.
5	-/
6	import Mathlib.Combinatorics.SimpleGraph.Clique
7
8	/-!
9	---
10	title: Connected matchings
11	type: definition
12	---
13	A connected matching is a matching whose distinct edges are joined by an edge.
14	Its maximum size is the connected-matching number $\mathrm{cm}(G)$ .
15	-/
16
17	namespace Lax342547.ConnectedMatching
18
19	universe u
20	variable {V : Type u}
21
22	/-- A finite matching whose edges are pairwise touching: each member is a
23	two-vertex clique, and distinct members are disjoint and joined by an edge. -/
24	def IsTouchingMatching (G : SimpleGraph V) (M : Finset (Finset V)) : Prop :=
25	(∀ e ∈ M, e.card = 2 ∧ G.IsClique (e : Set V)) ∧
26	(∀ e ∈ M, ∀ f ∈ M, e ≠ f → Disjoint e f) ∧
27	(∀ e ∈ M, ∀ f ∈ M, e ≠ f →
28	∃ v ∈ e, ∃ w ∈ f, G.Adj v w)
29
30	/-- The supremum of the cardinalities of pairwise touching matchings.
31	For finite vertex types, this supremum is attained. -/
32	noncomputable def connectedMatchingNumber (G : SimpleGraph V) : ℕ :=
33	sSup {n : ℕ \| ∃ M : Finset (Finset V), IsTouchingMatching G M ∧ M.card = n}
34
35	end Lax342547.ConnectedMatching
36

Builds on

none

Used by

From Mathlib

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

Loading discussion…

Lax Lean Archive