- D2167: Binomial coefficient
- R4777: Expectation of bounded random real number is within the bounding interval
- R2747: Finite sets are closed in Hausdorff space
- D371: Imaginary number
- R5564: Eigenvalue sequence for an upper triangular complex matrix
- R2079: Isotonicity of set intersection
- D3333: Hölder map
- D6268: 64-bit integer
- R1369: Jensen's inequality for expectation
- D4201: Set of rademacher integers