Prove2Me

Lemma 2 — any subset of an independent set is independent

Proved
WhitneyMatroid.RankIndep.indep_subset

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 MM, and call NN independent when its nullity vanishes, ρ(N)=r(N)\rho(N) = r(N). Then for all subsets N⊆N′N \subseteq N':

ρ(N′)=r(N′)  ⟹  ρ(N)=r(N).\rho(N') = r(N') \implies \rho(N) = r(N).

This is postulate (I₁) for the independent sets defined by a rank function, the first half of the deduction of (I) from (R).

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

/-- Lemma 2 (p. 510). Any subset of an independent set is independent. -/
theorem indep_subset {α : Type*} [Fintype α] [DecidableEq α]
    (r : Finset α → ℤ) (hr : IsRankSystem r) :
    ∀ N N' : Finset α, N ⊆ N' → indepOfRank r N' → indepOfRank r N := by sorry

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