Definition df-dde 34848

Description: Define the Dirac delta measure. (Contributed by Thierry Arnoux, 14-Sep-2018.)

Assertion

Ref	Expression
df-dde	⊢ δ = (𝑎 ∈ 𝒫 ℝ ↦ if(0 ∈ 𝑎, 1, 0))

Detailed syntax breakdown of Definition df-dde

Step	Hyp	Ref	Expression
1		cdde 34847	. 2 class δ
2		va	. . 3 setvar 𝑎
3		cr 11180	. . . 4 class ℝ
4	3	cpw 4557	. . 3 class 𝒫 ℝ
5		cc0 11181	. . . . 5 class 0
6	2	cv 1569	. . . . 5 class 𝑎
7	5, 6	wcel 2145	. . . 4 wff 0 ∈ 𝑎
8		c1 11182	. . . 4 class 1
9	7, 8, 5	cif 4482	. . 3 class if(0 ∈ 𝑎, 1, 0)
10	2, 4, 9	cmpt 5186	. 2 class (𝑎 ∈ 𝒫 ℝ ↦ if(0 ∈ 𝑎, 1, 0))
11	1, 10	wceq 1570	1 wff δ = (𝑎 ∈ 𝒫 ℝ ↦ if(0 ∈ 𝑎, 1, 0))

This definition is used by:  ddeval1  34849  ddeval0  34850  ddemeas  34851