Theorem 8 — an independent set extends to a base by elements of a given base

Proved

WhitneyMatroid.Duality.exists_subset_union_isBase

by mikedeng1 · 1 vote · Oct 5, 2026 · Mathlib 0df444a (Lean v4.33.1)

basesmatroidsp2o-batch-pfp2bp2o-gran-per-chapterp2o-plan-paperp2o-v1

Let $M$ be a matroid on a finite set of elements. If $B$ is a base of $M$ and $N$ is an independent set, then there is a subset $N'$ of $B$ such that

N \cup N' \ \text{ is a base of } M.

Any independent set can thus be completed to a base using only elements of a prescribed base. Whitney uses it in the proof of Theorem 23 to find a base of $M'$ with the maximal number of elements inside a given set.

Formalization Note The matroid is a Mathlib Matroid on a finite type with ground set the whole type; Whitney's $N+N'$ is the union $N\cup N'$ .

Preamble

import Mathlib
import Definitions.Def_WhitneyMatroid_Duality_IsDual

Formal statement

namespace WhitneyMatroid.Duality

/-- Whitney, Theorem 8 (p. 515): in a matroid `M` on a finite set of elements, if `B` is a base
and `N` is independent, then for some subset `N′` of `B`, `N + N′` is a base. -/
theorem exists_subset_union_isBase {α : Type*} [Finite α] (M : Matroid α)
    (hE : M.E = Set.univ) {B N : Set α} (hB : M.IsBase B) (hN : M.Indep N) :
    ∃ N' : Set α, N' ⊆ B ∧ M.IsBase (N ∪ N') := by sorry

end WhitneyMatroid.Duality

Source

Whitney, On the Abstract Properties of Linear Dependence, Amer. J. Math. 57 (1935), p. 515, Theorem 8

Human review

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

View graph