Local finiteness near compact support

Compact support of a differential form: Let $M$ be a smooth manifold, possibly with boundary, and $k\ge 0$. For $\omega \in {\mathrm{\Omega }}^k(M)$ define $\mathrm{supp}\omega ={\overline{\{p\in M:{\omega }_p\mathrm{\ne }0\}}}^M,{\mathrm{\Omega }}_c^k(M)=\{\omega \in {\mathrm{\Omega }}^k(M):\mathrm{supp}\omega \text{ is compact}\}\mathrm{.}$ The closure and compactness are in $M$, including its genuine boundary. Zero is the intrinsic zero of each exterior-power fiber, so this definition is independent of trivialization. The zero form has empty support.

Smooth partitions of unity subordinate to an open cover: Let $M$ be a smooth manifold and let $(U_i{)}_{i\in I}$ be an open cover of $M$. A family of smooth functions $({\varphi }_i{)}_{i\in I}$ with ${\varphi }_i:M\to [0,1]$ is a smooth partition of unity subordinate to $(U_i{)}_{i\in I}$ when: 1. the family $(\mathrm{supp}({\varphi }_i){)}_{i\in I}$ is locally finite; 2. $\mathrm{supp}({\varphi }_i)\subseteq U_i$ for every $i\in I$; and 3. ${\sum }_i{\varphi }_i(p)=1$ for every $p\in M$.

A subspace is compact exactly when every family of open subsets of the ambient space covering it, indexed or not, has finitely many members covering it: Let $(X,\mathcal{T})$ be a topological space (def-topological-space), let $A\subseteq X$ and let $(A,{\mathcal{T}}_A)$ be the subspace (def-subspace-topology-top). Then: 1. Compactness read in the ambient space. $A$ is a compact subset of $X$ (def-compact-space), that is $(A,{\mathcal{T}}_A)$ is a compact space, if and only if for every family $\mathcal{U}\subseteq \mathcal{T}$ with $A\subseteq \bigcup \mathcal{U}$ there are $n\in \mathbb{N}$ and $U_0,\dots ,U_n\in \mathcal{U}$ with $A\subseteq U_0\cup \cdots \cup U_n$, or else $A=\mathrm{\varnothing }$. 2. The same in indexed form. $A$ is a compact subset of $X$ if and only if for every set $I$ and every family $(U_i{)}_{i\in I}$ of open subsets of $X$ with $A\subseteq {\bigcup }_{i\in I}{U}_i$ there are $n\in \mathbb{N}$ and indices $i_0,\dots ,i_n\in I$ with $A\subseteq U_{i_0}\cup \cdots \cup U_{i_n}$, or else $A=\mathrm{\varnothing }$. Claim 2 is the form used by almost every later proof on this page, because a cover is usually produced by a rule that attaches an open set to each point or to each index, and a set of open sets forgets that rule. No choice principle is used anywhere below; the one place a selection is made is over a finite index set, and lem-finite-choice is a theorem of ZF.