Fixons une classe admissible $\mathscr{F}$ de fonctions numériques. Pour tout ouvert $U$ de $X$ et tout couple $(p,q)$ d’entiers naturels, notons $\mathscr{F}_{\text{pf}}^{p,q}(U)$ la limite inductive des espaces $\mathscr{F}^{p,q}_{P}(P)$, lorsque $(f\colon U\to T,P)$ parcourt l’ensemble des cartes tropicales sur $U$.

Lorsque $U$ parcourt l’ensemble des ouverts de $X$, les espaces $\mathscr{F}_{\text{pf}}^{p,q}(U)$ définissent un préfaisceau sur $X$  ; le faisceau associé $\mathscr{F}_{X}^{p,q}$, est appelé le faisceau des formes de type $(p,q)$ sur $X$ à coefficients dans $\mathscr{F}$  ; lorsque $\mathscr{F}=\mathscr{A}$, on parle de forme lisse.

Soit $U$ un ouvert de $X$ et soit $(f\colon U\to T,P)$ une carte tropicale sur $U$. Toute forme $\alpha$ appartenant à $\mathscr{F}^{p,q}_{P}(P)$ définit un élément de $\mathscr{F}^{p,q}_{\text{pf}}(U)$, puis une forme appartenant à $\mathscr{F}^{p,q}_{X}(U)$  ; celle-ci sera notée $f^{*}\alpha$.

Supposons que $\dim(X)<\max(p,q)$. Le faisceau $\mathscr{F}_{X}^{p,q}$ est alors nul. En effet, soit $U$ un ouvert de $X$, soit $(f\colon U\to T,P)$ une carte tropicale sur $U$, et soit $\alpha$ une forme de type $(p,q)$ sur $P$ à coefficients dans $\mathscr{F}$. Nous allons montrer que $f^{*}\alpha$ est nulle au voisinage de tout point de $U$, ce qui suffira à conclure.

Soit $x\in U$ et soit $V$ un voisinage analytique compact de $x$ dans $U$. La carte tropicale $(f|_{\mathring{V}}\colon\mathring{V}\to T,P)$ se factorise par $(f|_{\mathring{V}}\colon\mathring{V}\to T,f_{\text{trop}}(V))$.

Par conséquent, $f^{*}\alpha|_{\mathring{V}}=(f|_{\mathring{V}})^{*}(\alpha|_{f_{\text{trop}}(V)})$.

La dimension de $f_{\text{trop}}(V)$ est majorée par celle de $X$, et est donc strictement inférieure à $\max(p,q)$. Par conséquent, $\mathscr{F}^{p,q}_{f_{\text{trop}}(V)}=0$  ; dès lors, $\alpha|_{f_{\text{trop}}(V)}=0$ et $f^{*}\alpha|_{\mathring{V}}=0$, ce qui achève la démonstration.