- R76: Empty set is closed
- R5188:
- D4865: Fisher random unsigned real number
- D2011: Euclidean real covariance
- R4973: Bias-variance partition of mean square error for random basic real number
- D4493: Canonical singleton map
- D5116: Cogeometric random natural number
- D5524: Standard Poisson random natural number
- R2164: Law of the excluded middle in probability calculus
- R5301: Random unsigned basic number has zero correlation with the empty indicator