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 29629
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 29627 . 2 class a.e.
2 vm . . . . . . . . 9 setvar 𝑚
32cv 1474 . . . . . . . 8 class 𝑚
43cdm 5038 . . . . . . 7 class dom 𝑚
54cuni 4372 . . . . . 6 class dom 𝑚
6 va . . . . . . 7 setvar 𝑎
76cv 1474 . . . . . 6 class 𝑎
85, 7cdif 3537 . . . . 5 class ( dom 𝑚𝑎)
98, 3cfv 5804 . . . 4 class (𝑚‘( dom 𝑚𝑎))
10 cc0 9815 . . . 4 class 0
119, 10wceq 1475 . . 3 wff (𝑚‘( dom 𝑚𝑎)) = 0
1211, 6, 2copab 4642 . 2 class {⟨𝑎, 𝑚⟩ ∣ (𝑚‘( dom 𝑚𝑎)) = 0}
131, 12wceq 1475 1 wff a.e. = {⟨𝑎, 𝑚⟩ ∣ (𝑚‘( dom 𝑚𝑎)) = 0}
Colors of variables: wff setvar class
This definition is referenced by:  relae  29630  brae  29631  braew  29632
  Copyright terms: Public domain W3C validator