Definition df-ae 30302

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.)

Assertion

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

Distinct variable group:   m, a

Detailed syntax breakdown of Definition df-ae

Step	Hyp	Ref	Expression
1		cae 30300	. 2 class a.e.
2		vm	. . . . . . . . 9 setvar m
3	2	cv 1482	. . . . . . . 8 class m
4	3	cdm 5114	. . . . . . 7 class dom m
5	4	cuni 4436	. . . . . 6 class U. dom m
6		va	. . . . . . 7 setvar a
7	6	cv 1482	. . . . . 6 class a
8	5, 7	cdif 3571	. . . . 5 class ( U. dom m \ a )
9	8, 3	cfv 5888	. . . 4 class ( m ` ( U. dom m \ a ) )
10		cc0 9936	. . . 4 class 0
11	9, 10	wceq 1483	. . 3 wff ( m ` ( U. dom m \ a ) ) = 0
12	11, 6, 2	copab 4712	. 2 class { <. a , m >. | ( m ` ( U. dom m \ a ) ) = 0 }
13	1, 12	wceq 1483	1 wff a.e. = { <. a , m >. | ( m ` ( U. dom m \ a ) ) = 0 }

This definition is referenced by:  relae  30303  brae  30304  braew  30305