Lemma 5.1 (Brualdi), p. 6 — two bases $A, B$ admit a bijection $\pi : A \to B$ with $A - x + \pi(x)$ a base for all $x \in A$

Proved

CurvatureSubmod.LocalSearch.lemma_5_1

by mikedeng1 · Oct 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

base-exchangematroidp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1

Let $\mathcal M$ be a matroid on a finite ground set $X$ , and let $A$ and $B$ be two bases of $\mathcal M$ . Then there is a bijection $\pi : A \to B$ such that

A - x + \pi(x) \in \mathcal B(\mathcal M) \qquad \text{for all } x \in A.

This bijective exchange property, due to Brualdi (1969; see Schrijver, Combinatorial Optimization, Corollary 39.12a), indexes the single-element swaps between a local optimum and an optimal base that the local-search analysis compares.

Formalization Note The matroid is Mathlib's Matroid X with any ground set; $\pi$ is a function $X \to X$ that restricts to a bijection from $A$ onto $B$ (Set.BijOn). Mathlib has only the single-element exchange Matroid.IsBase.exchange.

Preamble

import Mathlib
import Definitions.Def_NonmonotoneSubmod_Shared_Submodular
import Definitions.Def_CurvatureSubmod_LocalSearch_Setting

Formal statement

namespace CurvatureSubmod.LocalSearch

/-- Lemma 5.1 (Brualdi), p. 6: two bases `A`, `B` of a matroid admit a bijection
`π : A → B` with `A − x + π(x)` a base for every `x ∈ A`. -/
theorem lemma_5_1 {X : Type} [Fintype X] [DecidableEq X] (M : Matroid X) (A B : Finset X)
    (hA : M.IsBase (↑A : Set X)) (hB : M.IsBase (↑B : Set X)) :
    ∃ π : X → X, Set.BijOn π (↑A : Set X) (↑B : Set X) ∧
      ∀ x ∈ A, M.IsBase (↑(insert (π x) (A.erase x)) : Set X) := by sorry

end CurvatureSubmod.LocalSearch

Source

Sviridenko, Vondrák, Ward, Optimal approximation for submodular and supermodular optimization with bounded curvature (SODA 2015 version, Oct. 9, 2014), p. 6, Lemma 5.1 (Brualdi [3])

Human review

Endorsed by Shuze Chen · Oct 9, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 9, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Lemma 5.1 (Brualdi), p. 6 — two bases A,BA, BA,B admit a bijection π:A→B\pi : A \to Bπ:A→B with A−x+π(x)A - x + \pi(x)A−x+π(x) a base for all x∈Ax \in Ax∈A

Lemma 5.1 (Brualdi), p. 6 — two bases $A, B$ admit a bijection $\pi : A \to B$ with $A - x + \pi(x)$ a base for all $x \in A$