Griesmer bound

Every binary linear $[n,k,d]$ code satisfiesPuncturing on the support of a minimum-weight codeword reduces the rank by one and leaves minimum distance at least $\lceil d/2\rceil$, which proves the bound inductively.