Theorem 3 — submodularity of rank, (3.2) and (3.3)

Proved

WhitneyMatroid.RankIndep.rank_submodular

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

combinatoricsmatroidsp2o-batch-pfp2bp2o-gran-per-chapterp2o-plan-paperp2o-v1submodularity

Let $r$ satisfy Whitney's rank postulates (R₁), (R₂), (R₃) on the subsets of a finite set, and let $\Delta(M, N) = r(M + N) - r(M)$ as in (3.1), with $+$ denoting union and $M_1 M_2$ intersection. Then

for all subsets $M, N_1, N_2$ : $\Delta(M + N_2, N_1) \le \Delta(M, N_1)$ ;
equivalently, (3.2): for all subsets $M, N_1, N_2$ ,

r(M + N_1 + N_2) \le r(M + N_1) + r(M + N_2) - r(M);

equivalently, (3.3): for all subsets $M_1, M_2$ ,

r(M_1 + M_2) \le r(M_1) + r(M_2) - r(M_1 M_2).

This is the submodular inequality for the rank function, derived here from the local postulates (R₁)–(R₃) alone. It is the central property of rank in Whitney's paper.

Formalization Note The paper states the first two forms as alternatives ("or") and calls (3.3) evidently equivalent; all three are asserted, as a conjunction. $M$ , $N_1$ , $N_2$ , $M_1$ , $M_2$ are arbitrary subsets, not only the whole matroid.

Preamble

import Mathlib
import Definitions.Def_WhitneyMatroid_RankIndep_Postulates

Formal statement

namespace WhitneyMatroid.RankIndep

/-- Theorem 3 (p. 511). `Δ(M + N₂, N₁) ≤ Δ(M, N₁)`, or, (3.2)
`r(M + N₁ + N₂) ≤ r(M + N₁) + r(M + N₂) − r(M)`; and the equivalent form (3.3)
`r(M₁ + M₂) ≤ r(M₁) + r(M₂) − r(M₁M₂)`. Here `+` is union and `M₁M₂` intersection. -/
theorem rank_submodular {α : Type*} [Fintype α] [DecidableEq α]
    (r : Finset α → ℤ) (hr : IsRankSystem r) :
    (∀ M N₁ N₂ : Finset α, Delta r (M ∪ N₂) N₁ ≤ Delta r M N₁) ∧
    (∀ M N₁ N₂ : Finset α, r (M ∪ N₁ ∪ N₂) ≤ r (M ∪ N₁) + r (M ∪ N₂) - r M) ∧
    (∀ M₁ M₂ : Finset α, r (M₁ ∪ M₂) ≤ r M₁ + r M₂ - r (M₁ ∩ M₂)) := by sorry

end WhitneyMatroid.RankIndep

Source

Whitney, On the Abstract Properties of Linear Dependence, Amer. J. Math. 57 (1935), p. 511, Theorem 3, (3.2), (3.3)

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