Lemma 6 — if e is dependent on P₁ but on no proper subset of P₁, then P₁ + e is a circuit

Proved

WhitneyMatroid.RankCircuit.circuit_of_minimal_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 $(\mathrm R_1)$ – $(\mathrm R_3)$ . Let $P_1 \subseteq M$ and $e \notin P_1$ . Suppose $e$ is dependent on $P_1$ , i.e. $r(P_1 + e) = r(P_1)$ , but on no proper subset of $P_1$ : $r(Q + e) \ne r(Q)$ for every $Q \subset P_1$ , $Q \neq P_1$ . Then

P = P_1 + e \ \text{ is a circuit of } r.

Together with Lemma 5 this is the bridge between dependence of an element on a set and circuits through that element (Theorem 4).

Formalization Note The hypothesis $e \notin P_1$ is tacit in the paper (it writes $P = P_1 + e$ and its proof uses $\rho(P_1) < \rho(P)$ ); it is added as a binder.

Preamble

import Mathlib
import Definitions.Def_WhitneyMatroid_RankCircuit_IsRankSystem

Formal statement

namespace WhitneyMatroid.RankCircuit

theorem circuit_of_minimal_dependent {α : Type*} [Fintype α] [DecidableEq α]
    (r : Finset α → ℤ) (hr : IsRankSystem r) (P₁ : Finset α) (e : α) (he : e ∉ P₁)
    (hdep : IsDependentOn r e P₁) (hmin : ∀ Q : Finset α, Q ⊂ P₁ → ¬ IsDependentOn r e Q) :
    circuitsOfRank r (insert e P₁) := by sorry

end WhitneyMatroid.RankCircuit

Source

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

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