Theorem 11 — rank additivity passes to subsets of the two parts

Proved

WhitneyMatroid.Components.rank_additive_of_subsets

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

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

Let $M$ be a finite matroid on a ground set $E$ with rank function $r$ , and let $M_1, M_2\subseteq E$ with

r(M_1 + M_2) = r(M_1) + r(M_2).

If $M_1'\subseteq M_1$ and $M_2'\subseteq M_2$ , then

r(M_1' + M_2') = r(M_1') + r(M_2').

Here $+$ denotes the union of sets. In words: if the rank of a union is the sum of the ranks of the two parts, the same holds for any choice of subsets of the two parts. This is the basic tool behind Theorems 12–19.

Formalization Note Whitney states the theorem for a matroid $M = M_1 + M_2$ ; here $M_1$ and $M_2$ are arbitrary subsets of the ground set of an ambient finite matroid, which is the same statement applied to the submatroid $M_1+M_2$ (rank in a submatroid is the induced rank). The parts are not required to be disjoint; Whitney writes $M_1+M_2$ also for overlapping sets (Theorem 13), and the statement holds in that generality. Ranks are Mathlib's M.eRk, finite here.

Preamble

import Mathlib

Formal statement

namespace WhitneyMatroid.Components

theorem rank_additive_of_subsets {α : Type*} (M : Matroid α) [M.Finite]
    (M₁ M₂ M₁' M₂' : Set α) (hM₁ : M₁ ⊆ M.E) (hM₂ : M₂ ⊆ M.E)
    (hr : M.eRk (M₁ ∪ M₂) = M.eRk M₁ + M.eRk M₂)
    (h₁ : M₁' ⊆ M₁) (h₂ : M₂' ⊆ M₂) :
    M.eRk (M₁' ∪ M₂') = M.eRk M₁' + M.eRk M₂' := by sorry

end WhitneyMatroid.Components

Source

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

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