QuantumInfo.Finite.Channel.DegradableOrder

For a fixed input space $\mathcal{H}_{in}$ (indexed by the finite type $dIn$), the degradable preorder is a preorder defined on the set of all quantum channels (CPTP maps) $\Lambda: \mathcal{L}(\mathcal{H}_{in}) \to \mathcal{L}(\mathcal{H}_{out})$ where the output space $\mathcal{H}_{out}$ can vary. Specifically, the carrier set consists of pairs $(dOut, \Lambda)$, where $dOut$ specifies the output dimension and its required structures (finite type and decidable equality), and $\Lambda$ is a CPTP map from $dIn$ to $dOut$. A channel $\Lambda_1$ is said to be less than or equal to $\Lambda_2$ ($\Lambda_1 \le \Lambda_2$) if $\Lambda_2$ is degradable to $\Lambda_1$. That is, $\Lambda_1 \le \Lambda_2$ if there exists a CPTP map $D: \mathcal{L}(\mathcal{H}_{out_2}) \to \mathcal{L}(\mathcal{H}_{out_1})$ such that $\Lambda_1 = D \circ \Lambda_2$.