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	⊢ a.e. = { ⟨ 𝑎 , 𝑚 ⟩ ∣ ( 𝑚 ‘ ( ∪ dom 𝑚 ∖ 𝑎 ) ) = 0 }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cae	⊢ a.e.
1		va	⊢ 𝑎
2		vm	⊢ 𝑚
3	2	cv	⊢ 𝑚
4	3	cdm	⊢ dom 𝑚
5	4	cuni	⊢ ∪ dom 𝑚
6	1	cv	⊢ 𝑎
7	5 6	cdif	⊢ ( ∪ dom 𝑚 ∖ 𝑎 )
8	7 3	cfv	⊢ ( 𝑚 ‘ ( ∪ dom 𝑚 ∖ 𝑎 ) )
9		cc0	⊢ 0
10	8 9	wceq	⊢ ( 𝑚 ‘ ( ∪ dom 𝑚 ∖ 𝑎 ) ) = 0
11	10 1 2	copab	⊢ { ⟨ 𝑎 , 𝑚 ⟩ ∣ ( 𝑚 ‘ ( ∪ dom 𝑚 ∖ 𝑎 ) ) = 0 }
12	0 11	wceq	⊢ a.e. = { ⟨ 𝑎 , 𝑚 ⟩ ∣ ( 𝑚 ‘ ( ∪ dom 𝑚 ∖ 𝑎 ) ) = 0 }