- D2950: Strict superlevel set
- D427: Isotone map
- R4328: Probability of finite union with an almost sure event
- D1676: Null set
- D520: Set exterior
- D1704: Complete measure
- R4333: Binary product of indicator functions equals indicator of intersection
- D47: Lipschitz map
- D1104: Binary relation structure
- R4654: Probability calculus expression for basic real conditional expectation given a complement partition of the sample space