The matching number of a relation between two lists

A matching of R : α → β → Prop between lists l and m pairs members of l with distinct members of m related to them: a sublist of l related pointwise by List.Forall₂ R to a subpermutation of m. List.matchingNumber R l m is the size of a largest matching.

Main definitions

• List.matchingNumber: the size of a largest matching of R between two lists.

Main results

• List.le_matchingNumber_iff: R has a matching of size k iff k ≤ matchingNumber R l m.
• List.countP_le_matchingNumber: the members of a duplicate-free list bearing a relation contained in R, and injective, to members of m are pairable.

def List.matchingNumber {α : Type u_1} {β : Type u_2} (R : α → β → Prop) [DecidableRel R] [DecidableEq β] : List α → List β → ℕ

The matching number of R between l and m, the most members of l that can be paired along R with distinct members of m. The head of l is either unpaired or paired with a member of m, which is then no longer available.

Equations

• List.matchingNumber R [] x✝ = 0
• List.matchingNumber R (a :: l) x✝ = max (List.matchingNumber R l x✝) ({b ∈ x✝.toFinset | R a b}.sup fun (b : β) => List.matchingNumber R l (x✝.erase b) + 1)

@[simp]

theorem List.matchingNumber_nil {α : Type u_1} {β : Type u_2} {R : α → β → Prop} [DecidableRel R] [DecidableEq β] (m : List β) : matchingNumber R [] m = 0

theorem List.matchingNumber_cons {α : Type u_1} {β : Type u_2} {R : α → β → Prop} [DecidableRel R] [DecidableEq β] (a : α) (l : List α) (m : List β) : matchingNumber R (a :: l) m = max (matchingNumber R l m) ({b ∈ m.toFinset | R a b}.sup fun (b : β) => matchingNumber R l (m.erase b) + 1)

theorem List.le_matchingNumber_iff {α : Type u_1} {β : Type u_2} {R : α → β → Prop} [DecidableRel R] [DecidableEq β] {l : List α} {m : List β} {k : ℕ} : k ≤ matchingNumber R l m ↔ ∃ (l₁ : List α) (m₁ : List β), l₁.Sublist l ∧ m₁.Subperm m ∧ Forall₂ R l₁ m₁ ∧ l₁.length = k

R has a matching of size k between l and m, a sublist of l of length k related by Forall₂ R to a subpermutation of m, exactly when k is at most the matching number.

theorem List.countP_le_matchingNumber {α : Type u_1} {β : Type u_2} {R : α → β → Prop} [DecidableRel R] [DecidableEq β] {l : List α} {S : α → β → Prop} [DecidableRel S] (hl : l.Nodup) (hSR : ∀ a ∈ l, ∀ (b : β), S a b → R a b) (hS : ∀ a ∈ l, ∀ a' ∈ l, ∀ (b : β), S a b → S a' b → a = a') (m : List β) : countP (fun (a : α) => decide (∃ b ∈ m, S a b)) l ≤ matchingNumber R l m

The members of a duplicate-free list bearing S to some member of m are pairable along R, where S is contained in R and no two members bear S to one member of m.