Metamath Proof Explorer

Definition df-dde

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

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

Detailed syntax breakdown

Step Hyp Ref Expression
0 cdde 
 |-  Ddelta
1 va 
 |-  a
2 cr 
 |-  RR
3 2 cpw 
 |-  ~P RR
4 cc0 
 |-  0
5 1 cv 
 |-  a
6 4 5 wcel 
 |-  0 e. a
7 c1 
 |-  1
8 6 7 4 cif 
 |-  if ( 0 e. a , 1 , 0 )
9 1 3 8 cmpt 
 |-  ( a e. ~P RR |-> if ( 0 e. a , 1 , 0 ) )
10 0 9 wceq 
 |-  Ddelta = ( a e. ~P RR |-> if ( 0 e. a , 1 , 0 ) )