Lemma 5 — each element of a circuit is dependent on the rest of the circuit

Proved

WhitneyMatroid.RankCircuit.circuit_elem_dependent

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

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

Let $r$ be a rank function on the subsets of a finite set $M$ satisfying Whitney's postulates $(\mathrm R_1)$ – $(\mathrm R_3)$ , and let $P$ be a circuit of $r$ , that is, a minimal set with positive nullity. Then for every element $e \in P$ , $e$ is dependent on $P - e$ :

r(P) = r(P - e).

This is the first step in reading off nullity from circuits; it underlies Theorem 4.

Preamble

import Mathlib
import Definitions.Def_WhitneyMatroid_RankCircuit_IsRankSystem

Formal statement

namespace WhitneyMatroid.RankCircuit

theorem circuit_elem_dependent {α : Type*} [Fintype α] [DecidableEq α]
    (r : Finset α → ℤ) (hr : IsRankSystem r) (P : Finset α) (hP : circuitsOfRank r P)
    (e : α) (he : e ∈ P) :
    IsDependentOn r e (P.erase e) := by sorry

end WhitneyMatroid.RankCircuit

Source

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

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