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	$$⊢\mathrm{ae}=\left\{⟨a,m⟩|m\left(\bigcup \mathrm{dom}m\setminus a\right)=0\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cae	$$class\mathrm{ae}$$
1		va	$$setvara$$
2		vm	$$setvarm$$
3	2	cv	$$setvarm$$
4	3	cdm	$$class\mathrm{dom}m$$
5	4	cuni	$$class\bigcup \mathrm{dom}m$$
6	1	cv	$$setvara$$
7	5 6	cdif	$$class\left(\bigcup \mathrm{dom}m\setminus a\right)$$
8	7 3	cfv	$$classm\left(\bigcup \mathrm{dom}m\setminus a\right)$$
9		cc0	$$class0$$
10	8 9	wceq	$$wffm\left(\bigcup \mathrm{dom}m\setminus a\right)=0$$
11	10 1 2	copab	$$class\left\{⟨a,m⟩|m\left(\bigcup \mathrm{dom}m\setminus a\right)=0\right\}$$
12	0 11	wceq	$$wff\mathrm{ae}=\left\{⟨a,m⟩|m\left(\bigcup \mathrm{dom}m\setminus a\right)=0\right\}$$