Formal immersion between smooth manifolds

Assume ${\mathrm{A}\mathrm{C}}_{\omega }$ for the smooth tangent-bundle constructions. Let $M^m$ and $N^n$ be smooth manifolds, with their canonical smooth tangent bundles (Assuming countable choice, the tangent bundle has a canonical smooth 2n-manifold structure, The induced tangent bundle chart, Tangent-bundle chart transitions are smooth with smooth inverses) and smooth global differential (Assuming countable choice, the global differential of a smooth map is smooth). A formal immersion from $M$ to $N$ is a pair $(f,F)$ in which $f:M\to N$ is a smooth map and $F:TM\to TN$ is a smooth bundle map over $f$, meaning ${\pi }_N\circ F=f\circ {\pi }_M$ where ${\pi }_M,{\pi }_N$ are the bundle projections, and $F_x:=F{\mathrm{\mid }}_{T_{x}M}:T_{x}M\to T_{f(x)}N$ is injective for every $x\in M$. The pair is a formal immersion of rank $m$ into rank $n$, so, when $M$ is nonempty, necessarily $m\le n$; equality of ranks is allowed and makes each $F_x$ a linear isomorphism. A smooth map $f$ is an immersion exactly when $(f,df)$ is a formal immersion; no orientation, metric, framing or properness is part of the datum. If $M$ is empty the unique pair satisfies the fibre condition vacuously, irrespective of the dimensions.