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 30636
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 30634 . 2 class a.e.
2 vm . . . . . . . . 9 setvar 𝑚
32cv 1629 . . . . . . . 8 class 𝑚
43cdm 5249 . . . . . . 7 class dom 𝑚
54cuni 4572 . . . . . 6 class dom 𝑚
6 va . . . . . . 7 setvar 𝑎
76cv 1629 . . . . . 6 class 𝑎
85, 7cdif 3718 . . . . 5 class ( dom 𝑚𝑎)
98, 3cfv 6031 . . . 4 class (𝑚‘( dom 𝑚𝑎))
10 cc0 10137 . . . 4 class 0
119, 10wceq 1630 . . 3 wff (𝑚‘( dom 𝑚𝑎)) = 0
1211, 6, 2copab 4844 . 2 class {⟨𝑎, 𝑚⟩ ∣ (𝑚‘( dom 𝑚𝑎)) = 0}
131, 12wceq 1630 1 wff a.e. = {⟨𝑎, 𝑚⟩ ∣ (𝑚‘( dom 𝑚𝑎)) = 0}
Colors of variables: wff setvar class
This definition is referenced by:  relae  30637  brae  30638  braew  30639
  Copyright terms: Public domain W3C validator