Definition df-dde 30296

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

Assertion

Ref	Expression
df-dde	|- δ = ( a e. ~P RR |-> if ( 0 e. a , 1 , 0 ) )

Detailed syntax breakdown of Definition df-dde

Step	Hyp	Ref	Expression
1		cdde 30295	. 2 class δ
2		va	. . 3 setvar a
3		cr 9935	. . . 4 class RR
4	3	cpw 4158	. . 3 class ~P RR
5		cc0 9936	. . . . 5 class 0
6	2	cv 1482	. . . . 5 class a
7	5, 6	wcel 1990	. . . 4 wff 0 e. a
8		c1 9937	. . . 4 class 1
9	7, 8, 5	cif 4086	. . 3 class if ( 0 e. a , 1 , 0 )
10	2, 4, 9	cmpt 4729	. 2 class ( a e. ~P RR |-> if ( 0 e. a , 1 , 0 ) )
11	1, 10	wceq 1483	1 wff δ = ( a e. ~P RR |-> if ( 0 e. a , 1 , 0 ) )

This definition is referenced by:  ddeval1  30297  ddeval0  30298  ddemeas  30299