ThmDex – An index of mathematical definitions, results, and conjectures.
Result R3938 on D198: Probability measure
Upper and lower bounds for codomain set of probability measure
Formulation 0
Let $M = (\Omega, \mathcal{F})$ be a D1108: Measurable space.
Let $\mathbb{P} : \mathcal{F} \to [0, \infty]$ be a D198: Probability measure on $M$.
Then \begin{equation} \mathbb{P}(\mathcal{F}) \subseteq [0, 1] \end{equation}
Formulation 1
Let $M = (\Omega, \mathcal{F})$ be a D1108: Measurable space.
Let $\mathbb{P} : \mathcal{F} \to [0, \infty]$ be a D198: Probability measure on $M$.
Then \begin{equation} 0 \leq \mathbb{P} \leq 1 \end{equation}
Proofs
Proof 0
Let $M = (\Omega, \mathcal{F})$ be a D1108: Measurable space.
Let $\mathbb{P} : \mathcal{F} \to [0, \infty]$ be a D198: Probability measure on $M$.
Since, by definition, $\mathbb{P}(\Omega) = 1$, this result is a particular case of R3939: Upper and lower bounds for codomain set of finite unsigned basic measure. $\square$