ext φ
R : Type u_1
inst✝¹⁰ : RealScalar R
W : Type ?u.28987
inst✝⁹ : Vec R W
inst✝⁸ : Module ℝ W
X : Type u_2
inst✝⁷ : SemiHilbert R X
inst✝⁶ : MeasureSpace X
Y : Type u_3
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.30863
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type ?u.31781
inst✝¹ : Vec R U
V : Type ?u.31802
inst✝ : Vec R V
f : X → Y
x : X
⊢ surfaceDirac {x} f 0 = Distribution.postComp (dirac x) (fun r ⊸[R] r • f x)
case a
R : Type u_1
inst✝¹⁰ : RealScalar R
W : Type ?u.28987
inst✝⁹ : Vec R W
inst✝⁸ : Module ℝ W
X : Type u_2
inst✝⁷ : SemiHilbert R X
inst✝⁶ : MeasureSpace X
Y : Type u_3
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.30863
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type ?u.31781
inst✝¹ : Vec R U
V : Type ?u.31802
inst✝ : Vec R V
f : X → Y
x : X
φ : 𝒟 X
⊢ (surfaceDirac {x} f 0) φ = (Distribution.postComp (dirac x) (fun r ⊸[R] r • f x)) φ