§4 — the independent sets of a rank system satisfy (I₂)

Proved

WhitneyMatroid.RankIndep.indepOfRank_augment

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 call $N$ independent when $\rho(N) = r(N)$ , $\rho$ counting elements. Then the independent sets satisfy postulate (I₂): if $N$ and $N'$ are independent and $N'$ has exactly one element more than $N$ ,

\rho(N') = \rho(N) + 1,

then there is an element $e' \in N'$ with $e' \notin N$ such that $N + e'$ is independent.

Together with Lemma 2, this deduces the independence postulates (I) from the rank postulates (R), one half of Whitney's equivalence theorem.

Preamble

import Mathlib
import Definitions.Def_WhitneyMatroid_RankIndep_Postulates

Formal statement

namespace WhitneyMatroid.RankIndep

/-- §4 (pp. 511–512). Under (R₁), (R₂), (R₃), the independent sets `n(N) = 0` satisfy (I₂). -/
theorem indepOfRank_augment {α : Type*} [Fintype α] [DecidableEq α]
    (r : Finset α → ℤ) (hr : IsRankSystem r) :
    IndepI2 (indepOfRank r) := by sorry

end WhitneyMatroid.RankIndep

Source

Whitney, On the Abstract Properties of Linear Dependence, Amer. J. Math. 57 (1935), pp. 511–512, §4 (deduction of (I₂) from (R₁), (R₂), (R₃))

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