Let $X$ be a real normed space and $k \ge 0$. Mathlib's Grassmannian $G(k, X; \mathbb{R})$ is the algebro-geometric one: over the field $\mathbb{R}$ its points are the subspaces $N \le X$ of codimension $k$, closed or not. The Grassmannian $\mathcal{G}^k X$ of the concept $BanachGrassmannian$ consists of the closed subspaces of codimension $k$, each of which admits a bounded projection, and carries a metric. The map $V \mapsto V$ identifies $\mathcal{G}^k X$ with the subspaces in $G(k, X; \mathbb{R})$ that are closed in $X$.