constructor
R : Type u_3
C : Type u_1
inst✝² : Scalar R C
W : Type ?u.3169
inst✝¹ : Vec C W
U : Type u_2
inst✝ : SemiInnerProductSpace C U
x✝ : U → C
hx : HasAdjDiff C x✝
x : U
⊢ HasAdjDiffAt C (fun u => sin (x✝ u)) x
case left
R : Type u_3
C : Type u_1
inst✝² : Scalar R C
W : Type ?u.3169
inst✝¹ : Vec C W
U : Type u_2
inst✝ : SemiInnerProductSpace C U
x✝ : U → C
hx : HasAdjDiff C x✝
x : U
⊢ CDifferentiableAt C (fun u => sin (x✝ u)) x

case right
R : Type u_3
C : Type u_1
inst✝² : Scalar R C
W : Type ?u.3169
inst✝¹ : Vec C W
U : Type u_2
inst✝ : SemiInnerProductSpace C U
x✝ : U → C
hx : HasAdjDiff C x✝
x : U
⊢ HasSemiAdjoint C (cderiv C (fun u => sin (x✝ u)) x)