Theorem boolesineq

Description: Boole's inequality (union bound). For any finite or countable collection of events, the probability of their union is at most the sum of their probabilities. (Suggested by DeepSeek R1.) (Contributed by Ender Ting, 30-Apr-2025)

	Ref	Expression
Assertion	boolesineq	|- ( ( P e. Prob /\ A : NN --> dom P ) -> ( P ` U_ n e. NN ( A ` n ) ) <_ sum* n e. NN ( P ` ( A ` n ) ) )

Proof

Step	Hyp	Ref	Expression
1		domprobmeas	|- ( P e. Prob -> P e. ( measures ` dom P ) )
2	1	adantr	|- ( ( P e. Prob /\ A : NN --> dom P ) -> P e. ( measures ` dom P ) )
3		domprobsiga	|- ( P e. Prob -> dom P e. U. ran sigAlgebra )
4		simpr	|- ( ( P e. Prob /\ A : NN --> dom P ) -> A : NN --> dom P )
5	4	ffvelcdmda	|- ( ( ( P e. Prob /\ A : NN --> dom P ) /\ n e. NN ) -> ( A ` n ) e. dom P )
6	5	ralrimiva	|- ( ( P e. Prob /\ A : NN --> dom P ) -> A. n e. NN ( A ` n ) e. dom P )
7		sigaclcu2	|- ( ( dom P e. U. ran sigAlgebra /\ A. n e. NN ( A ` n ) e. dom P ) -> U_ n e. NN ( A ` n ) e. dom P )
8	3 6 7	syl2an2r	|- ( ( P e. Prob /\ A : NN --> dom P ) -> U_ n e. NN ( A ` n ) e. dom P )
9		ssidd	|- ( ( P e. Prob /\ A : NN --> dom P ) -> U_ n e. NN ( A ` n ) C_ U_ n e. NN ( A ` n ) )
10	2 8 5 9	measiun	|- ( ( P e. Prob /\ A : NN --> dom P ) -> ( P ` U_ n e. NN ( A ` n ) ) <_ sum* n e. NN ( P ` ( A ` n ) ) )