Theorem 21 — duality is symmetric

Proved

WhitneyMatroid.Duality.isDual_symm

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

dualitymatroidsp2o-batch-pfp2bp2o-gran-per-chapterp2o-plan-paperp2o-v1

Let $M$ and $M'$ be matroids on finite sets of elements. If $M'$ is a dual of $M$ (in the sense of (11.1)), then $M$ is a dual of $M'$ :

M' \text{ dual of } M \ \Longrightarrow\ M \text{ dual of } M'.

So one may speak of $M$ and $M'$ simply as duals, as Theorems 23 and 28 do.

Formalization Note "Dual" is IsDual, (11.1) for some one-to-one correspondence between the elements; the correspondence in the conclusion may be any bijection (Whitney's proof uses the inverse of the given one).

Preamble

import Mathlib
import Definitions.Def_WhitneyMatroid_Duality_IsDual

Formal statement

namespace WhitneyMatroid.Duality

/-- Whitney, Theorem 21 (p. 522): if `M′` is a dual of `M`, then `M` is a dual of `M′`. -/
theorem isDual_symm {α β : Type*} [Finite α] [Finite β] {M : Matroid α} {M' : Matroid β}
    (h : IsDual M M') : IsDual M' M := by sorry

end WhitneyMatroid.Duality

Source

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

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