Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-ae Structured version   Visualization version   GIF version

Definition df-ae 30818
Description: Define 'almost everywhere' with regard to a measure 𝑀. 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. = {⟨𝑎, 𝑚⟩ ∣ (𝑚‘( dom 𝑚𝑎)) = 0}
Distinct variable group:   𝑚,𝑎

Detailed syntax breakdown of Definition df-ae
StepHypRef Expression
1 cae 30816 . 2 class a.e.
2 vm . . . . . . . . 9 setvar 𝑚
32cv 1652 . . . . . . . 8 class 𝑚
43cdm 5312 . . . . . . 7 class dom 𝑚
54cuni 4628 . . . . . 6 class dom 𝑚
6 va . . . . . . 7 setvar 𝑎
76cv 1652 . . . . . 6 class 𝑎
85, 7cdif 3766 . . . . 5 class ( dom 𝑚𝑎)
98, 3cfv 6101 . . . 4 class (𝑚‘( dom 𝑚𝑎))
10 cc0 10224 . . . 4 class 0
119, 10wceq 1653 . . 3 wff (𝑚‘( dom 𝑚𝑎)) = 0
1211, 6, 2copab 4905 . 2 class {⟨𝑎, 𝑚⟩ ∣ (𝑚‘( dom 𝑚𝑎)) = 0}
131, 12wceq 1653 1 wff a.e. = {⟨𝑎, 𝑚⟩ ∣ (𝑚‘( dom 𝑚𝑎)) = 0}
Colors of variables: wff setvar class
This definition is referenced by:  relae  30819  brae  30820  braew  30821
  Copyright terms: Public domain W3C validator