Theorem 4 — a circuit in N + e contains e iff e is dependent on N

Proved

WhitneyMatroid.RankCircuit.exists_circuit_iff_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 $N \subseteq M$ and let $e \notin N$ . Then

\bigl(\exists \text{ a circuit } P \subseteq N + e \text{ with } e \in P\bigr) \iff r(N + e) = r(N).

This expresses dependence of an element on a set purely in terms of circuits, which is what makes the rank recoverable from the circuits (Theorem 5 and §8).

Preamble

import Mathlib
import Definitions.Def_WhitneyMatroid_RankCircuit_IsRankSystem

Formal statement

namespace WhitneyMatroid.RankCircuit

theorem exists_circuit_iff_dependent {α : Type*} [Fintype α] [DecidableEq α]
    (r : Finset α → ℤ) (hr : IsRankSystem r) (N : Finset α) (e : α) (he : e ∉ N) :
    (∃ P : Finset α, circuitsOfRank r P ∧ P ⊆ insert e N ∧ e ∈ P) ↔ IsDependentOn r e N := by sorry

end WhitneyMatroid.RankCircuit

Source

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

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