Corollary: Data processing

For every further CPTP map $\Gamma$,

Exactly agreeing channels are closed under post-processing. For subsystem interfaces the agreement family

is a down-set.

Proof. Use Lemma lem:contract. For $S^{\prime }\subseteq S$, restriction to $S^{\prime }$ is a further partial trace after restriction to $S$.