![]() |
Mathbox for Thierry Arnoux |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > df-ae | Structured version Visualization version GIF version |
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.) |
Ref | Expression |
---|---|
df-ae | ⊢ a.e. = {⟨𝑎, 𝑚⟩ ∣ (𝑚‘(∪ dom 𝑚 ∖ 𝑎)) = 0} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cae 32900 | . 2 class a.e. | |
2 | vm | . . . . . . . . 9 setvar 𝑚 | |
3 | 2 | cv 1541 | . . . . . . . 8 class 𝑚 |
4 | 3 | cdm 5637 | . . . . . . 7 class dom 𝑚 |
5 | 4 | cuni 4869 | . . . . . 6 class ∪ dom 𝑚 |
6 | va | . . . . . . 7 setvar 𝑎 | |
7 | 6 | cv 1541 | . . . . . 6 class 𝑎 |
8 | 5, 7 | cdif 3911 | . . . . 5 class (∪ dom 𝑚 ∖ 𝑎) |
9 | 8, 3 | cfv 6500 | . . . 4 class (𝑚‘(∪ dom 𝑚 ∖ 𝑎)) |
10 | cc0 11059 | . . . 4 class 0 | |
11 | 9, 10 | wceq 1542 | . . 3 wff (𝑚‘(∪ dom 𝑚 ∖ 𝑎)) = 0 |
12 | 11, 6, 2 | copab 5171 | . 2 class {⟨𝑎, 𝑚⟩ ∣ (𝑚‘(∪ dom 𝑚 ∖ 𝑎)) = 0} |
13 | 1, 12 | wceq 1542 | 1 wff a.e. = {⟨𝑎, 𝑚⟩ ∣ (𝑚‘(∪ dom 𝑚 ∖ 𝑎)) = 0} |
Colors of variables: wff setvar class |
This definition is referenced by: relae 32903 brae 32904 braew 32905 |
Copyright terms: Public domain | W3C validator |