Lemma 8 — the circuit rank of a set is independent of the ordering of its elements

Proved

WhitneyMatroid.RankCircuit.rankSeq_perm

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

circuitsmatroidsp2o-batch-pfp2bp2o-gran-per-chapterp2o-plan-paperp2o-v1rank-function

Let the subsets of a finite set $M$ be divided into circuits and non-circuits so that $(\mathrm C_1)$ and $(\mathrm C_2)$ hold, and let $r(e_1, \dots, e_p) = \sum_i \Gamma_i$ be the rank of an ordered list defined from circuits. If $(e_1, \dots, e_p)$ has no repetitions and $(f_1, \dots, f_p)$ is a reordering of it, then

r(e_1, \dots, e_p) = r(f_1, \dots, f_p).

Hence the rank of a subset defined from circuits is well defined, independent of the chosen enumeration of its elements.

Formalization Note Orderings of the elements of $N$ are duplicate-free lists; "reordering" is List.Perm.

Preamble

import Mathlib
import Definitions.Def_WhitneyMatroid_RankCircuit_IsCircuitSystem

Formal statement

namespace WhitneyMatroid.RankCircuit

theorem rankSeq_perm {α : Type*} [Fintype α] [DecidableEq α]
    (C : Finset α → Prop) (hC : IsCircuitSystem C) (l₁ l₂ : List α) (hnd : l₁.Nodup)
    (hperm : l₁.Perm l₂) :
    rankSeq C l₁ = rankSeq C l₂ := by sorry

end WhitneyMatroid.RankCircuit

Source

Whitney, On the Abstract Properties of Linear Dependence, Amer. J. Math. 57 (1935), p. 517, Lemma 8

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