Definition df-dde

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

	Ref	Expression
Assertion	df-dde	$$⊢\delta =\left(a\in 𝒫ℝ⟼if\left(0\in a,1,0\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cdde	$$class\delta$$
1		va	$$setvara$$
2		cr	$$classℝ$$
3	2	cpw	$$class𝒫ℝ$$
4		cc0	$$class0$$
5	1	cv	$$setvara$$
6	4 5	wcel	$$wff0\in a$$
7		c1	$$class1$$
8	6 7 4	cif	$$classif\left(0\in a,1,0\right)$$
9	1 3 8	cmpt	$$class\left(a\in 𝒫ℝ⟼if\left(0\in a,1,0\right)\right)$$
10	0 9	wceq	$$wff\delta =\left(a\in 𝒫ℝ⟼if\left(0\in a,1,0\right)\right)$$