Definition df-ae

Description: Define 'almost everywhere' with regard to a measure M . A property holds almost everywhere if the measure of the set where it does not hold has measure zero. (Contributed by Thierry Arnoux, 20-Oct-2017)

	Ref	Expression
Assertion	df-ae	|- ae = { <. a , m >. | ( m ` ( U. dom m \ a ) ) = 0 }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cae	|- ae
1		va	|- a
2		vm	|- m
3	2	cv	|- m
4	3	cdm	|- dom m
5	4	cuni	|- U. dom m
6	1	cv	|- a
7	5 6	cdif	|- ( U. dom m \ a )
8	7 3	cfv	|- ( m ` ( U. dom m \ a ) )
9		cc0	|- 0
10	8 9	wceq	|- ( m ` ( U. dom m \ a ) ) = 0
11	10 1 2	copab	|- { <. a , m >. | ( m ` ( U. dom m \ a ) ) = 0 }
12	0 11	wceq	|- ae = { <. a , m >. | ( m ` ( U. dom m \ a ) ) = 0 }