Lemma 3 — $\Delta(M + e_2, e_1) \le \Delta(M, e_1)$

Proved

WhitneyMatroid.RankIndep.delta_insert_le

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

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

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. For every subset $M$ and all elements $e_1, e_2$ ,

\Delta(M + e_2, e_1) \le \Delta(M, e_1).

The gain in rank from adding $e_1$ does not increase when $e_2$ is added first. This is the one-element case of Lemma 4 and of the submodularity inequality, Theorem 3.

Formalization Note No hypothesis on $e_1, e_2$ is imposed: the paper does not restrict them, and when $e_1$ or $e_2$ already lies in $M$ , or $e_1 = e_2$ , the inequality still holds as stated. $\Delta(M, e)$ is $\Delta(M, \{e\})$ .

Preamble

import Mathlib
import Definitions.Def_WhitneyMatroid_RankIndep_Postulates

Formal statement

namespace WhitneyMatroid.RankIndep

/-- Lemma 3 (p. 511). `Δ(M + e₂, e₁) ≤ Δ(M, e₁)`, for any subset `M` and elements `e₁, e₂`. -/
theorem delta_insert_le {α : Type*} [Fintype α] [DecidableEq α]
    (r : Finset α → ℤ) (hr : IsRankSystem r) :
    ∀ (M : Finset α) (e₁ e₂ : α), Delta r (insert e₂ M) {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 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

Lemma 3 — Δ(M+e2,e1)≤Δ(M,e1)\Delta(M + e_2, e_1) \le \Delta(M, e_1)Δ(M+e2​,e1​)≤Δ(M,e1​)

Lemma 3 — $\Delta(M + e_2, e_1) \le \Delta(M, e_1)$