Countable basis support lemma (source code)

= Countable basis support lemma
{title2=$N\subseteq\langle E'\rangle,\quad E'\subseteq E\text{ countable}$}

A <submodule> $N$ of a <free module> with <basis of a module> $E$, generated by a <countable set>, is contained in the <submodule> generated by some <countable> subset $E'\subseteq E$. Take $E'$ to be the union of the finite <coordinate supports in a free module> of a countable generating family for $N$. This union is <countable>, and every generator belongs to $\langle E'\rangle$, which proves the inclusion. Combining this with <basis partition gives a module direct sum> places $N$ inside a countably generated <direct summand>.