Prove2Me

Lemma 4 — Δ(M+N,e)≤Δ(M,e)\Delta(M + N, e) \le \Delta(M, e)

Proved
WhitneyMatroid.RankIndep.delta_union_le

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

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

Let rr satisfy Whitney's rank postulates (R₁), (R₂), (R₃) on the subsets of a finite set, and let Δ(M,N)=r(M+N)−r(M)\Delta(M, N) = r(M + N) - r(M) as in (3.1), with ++ denoting union. For all subsets M,NM, N and every element ee,

Δ(M+N,e)≤Δ(M,e).\Delta(M + N, e) \le \Delta(M, e).

Adding any set NN beforehand can only decrease the rank gained by adding a single element ee. Lemma 4 is the step from Lemma 3 to the submodularity of rank (Theorem 3) and is used again in the deduction of (I₂) in §4.

Preamble
import Mathlib
import Definitions.Def_WhitneyMatroid_RankIndep_Postulates
Formal statement
namespace WhitneyMatroid.RankIndep

/-- Lemma 4 (p. 511). `Δ(M + N, e) ≤ Δ(M, e)`, for any subsets `M, N` and element `e`. -/
theorem delta_union_le {α : Type*} [Fintype α] [DecidableEq α]
    (r : Finset α → ℤ) (hr : IsRankSystem r) :
    ∀ (M N : Finset α) (e : α), Delta r (M ∪ N) {e} ≤ Delta r M {e} := by sorry

end WhitneyMatroid.RankIndep
Source
Whitney, On the Abstract Properties of Linear Dependence, Amer. J. Math. 57 (1935), p. 511, Lemma 4
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