Definition df-dde

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cdde	⊢ δ
1		va	⊢ 𝑎
2		cr	⊢ ℝ
3	2	cpw	⊢ 𝒫 ℝ
4		cc0	⊢ 0
5	1	cv	⊢ 𝑎
6	4 5	wcel	⊢ 0 ∈ 𝑎
7		c1	⊢ 1
8	6 7 4	cif	⊢ if ( 0 ∈ 𝑎 , 1 , 0 )
9	1 3 8	cmpt	⊢ ( 𝑎 ∈ 𝒫 ℝ ↦ if ( 0 ∈ 𝑎 , 1 , 0 ) )
10	0 9	wceq	⊢ δ = ( 𝑎 ∈ 𝒫 ℝ ↦ if ( 0 ∈ 𝑎 , 1 , 0 ) )