Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-dde Structured version   Visualization version   GIF version

Definition df-dde 31391
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
StepHypRef Expression
1 cdde 31390 . 2 class δ
2 va . . 3 setvar 𝑎
3 cr 10524 . . . 4 class
43cpw 4535 . . 3 class 𝒫 ℝ
5 cc0 10525 . . . . 5 class 0
62cv 1527 . . . . 5 class 𝑎
75, 6wcel 2105 . . . 4 wff 0 ∈ 𝑎
8 c1 10526 . . . 4 class 1
97, 8, 5cif 4463 . . 3 class if(0 ∈ 𝑎, 1, 0)
102, 4, 9cmpt 5137 . 2 class (𝑎 ∈ 𝒫 ℝ ↦ if(0 ∈ 𝑎, 1, 0))
111, 10wceq 1528 1 wff δ = (𝑎 ∈ 𝒫 ℝ ↦ if(0 ∈ 𝑎, 1, 0))
Colors of variables: wff setvar class
This definition is referenced by:  ddeval1  31392  ddeval0  31393  ddemeas  31394
  Copyright terms: Public domain W3C validator