Theorem 28 — orthogonal subspaces have dual associated matroids

Let $H$ be a hyperplane through the origin (a linear subspace) of $n$-dimensional Euclidean space $E_n$, of dimension $r$, and let $H' = H^\perp$ be the orthogonal hyperplane through the origin, of dimension $n-r$. Let $M$ and $M'$ be the matroids associated with $H$ and $H'$: both have elements $e_1,\dots,e_n$, one per coordinate, and a set $S$ of coordinates has rank in $M$ (resp. $M'$) equal to the dimension of the projection of $H$ (resp. $H'$) onto the coordinate subspace of the coordinates in $S$. Then $M$ and $M'$ are duals under the correspondence of equal coordinates: for every set $N$ of coordinates, with $N'$ its complement,

Equivalently, the column matroid of a real matrix and the column matroid of a matrix whose rows span the orthogonal complement of its row space are dual matroids. This is the linear-algebra model of Whitney's abstract duality.

Formalization Note $E_n$ is EuclideanSpace ℝ (Fin n) with its standard inner product and $H^\perp$ is Mathlib's orthogonal complement Hᗮ. "Associated" is the predicate IsAssociated (ground set all of Fin n, rank of every subset equal to the dimension of the coordinate projection of the subspace). The dimensions $r$ and $n-r$ are not hypotheses: they are consequences of $H' = H^\perp$. The statement covers $H=\{0\}$ and $H=E_n$ and $n=0$. The correspondence is the identity of the coordinate set, as in Whitney's proof.