§5 — the circuits of a rank system satisfy (C₁) and (C₂)

Proved

WhitneyMatroid.RankCircuit.circuitSystem_of_rankSystem

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

circuit-eliminationcircuitsmatroidsp2o-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)$ . Then its circuits (minimal sets of positive nullity) satisfy the circuit postulates:

$(\mathrm C_1)$ no proper subset of a circuit is a circuit;
$(\mathrm C_2)$ if $P_1, P_2$ are circuits, $e_1 \in P_1 \cap P_2$ and $e_2 \in P_1 \setminus P_2$ , then there is a circuit $P_3 \subseteq P_1 \cup P_2$ with $e_2 \in P_3$ and $e_1 \notin P_3$ .

This is the deduction of the circuit postulates from the rank postulates, one half of the equivalence of the two systems.

Preamble

import Mathlib
import Definitions.Def_WhitneyMatroid_RankCircuit_IsRankSystem
import Definitions.Def_WhitneyMatroid_RankCircuit_IsCircuitSystem

Formal statement

namespace WhitneyMatroid.RankCircuit

theorem circuitSystem_of_rankSystem {α : Type*} [Fintype α] [DecidableEq α]
    (r : Finset α → ℤ) (hr : IsRankSystem r) :
    IsCircuitSystem (circuitsOfRank r) := by sorry

end WhitneyMatroid.RankCircuit

Source

Whitney, On the Abstract Properties of Linear Dependence, Amer. J. Math. 57 (1935), pp. 512–513, §5 (Deduction of (C₁), (C₂) from (R₁), (R₂), (R₃))

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