Let $U \subset \mathbb{R}^n$ be open, let $m \in \mathbb{R}$, and let $A \in \Psi^m(U)$ be a properly supported pseudodifferential operator. Let $(x_0,\xi_0) \in T^*U \setminus 0$, and suppose that $A$ is elliptic at $(x_0,\xi_0)$. Then, for every distribution $u \in \mathcal{D}'(U)$,

\begin{align*} (x_0,\xi_0) \notin \operatorname{WF}(Au) \implies (x_0,\xi_0) \notin \operatorname{WF}(u). \end{align*}

Equivalently, microlocal smoothness of $Au$ at $(x_0,\xi_0)$ implies microlocal smoothness of $u$ at $(x_0,\xi_0)$.

If $A$ is not assumed properly supported, the same conclusion holds in the localized sense: after choosing compactly supported cutoffs $\psi,\chi \in C_c^\infty(U)$ with $\psi = 1$ on a neighbourhood of $x_0$ and $\chi = 1$ on a smaller neighbourhood of $x_0$, the assertion is applied to the locally defined operator $\chi A\psi$.