Let $X$ be a second-countable smooth manifold, let $T^*X \setminus 0$ denote its cotangent bundle with the zero section removed, let $m \in \mathbb{R}$, and let $P \in \Psi_{\mathrm{prop}}^m(X)$ be a properly supported scalar pseudodifferential operator of order $m$, regarded as a continuous map $P: \mathcal{D}'(X) \to \mathcal{D}'(X)$. For each $r \in \mathbb{R}$, let $H_{\mathrm{loc}}^r(X)$ denote the local [Sobolev space](/page/Sobolev%20Space) of order $r$, and define $WF^r(v) \subset T^*X \setminus 0$ for $v \in \mathcal{D}'(X)$ by declaring $\rho \notin WF^r(v)$ iff there exists $A \in \Psi_{\mathrm{prop}}^0(X)$ elliptic at $\rho$ such that $Av \in H_{\mathrm{loc}}^r(X)$. Let $\sigma_m(P)$ denote the homogeneous principal symbol of $P$, and let $\operatorname{Char}(P) \subset T^*X \setminus 0$ be the conic set on which $\sigma_m(P)$ is not elliptic. Let $\Psi^{-\infty}(X) := \bigcap_{N \in \mathbb{R}} \Psi^N(X)$ denote the class of smoothing pseudodifferential operators. Then for every distribution $u \in \mathcal{D}'(X)$ and every $s \in \mathbb{R}$,

\begin{align*} WF^s(u) \subset WF^{s-m}(Pu) \cup \operatorname{Char}(P). \end{align*}