fun_prop
X✝ : Type ?u.13303
R : Type u_1
inst✝³ : RealScalar R
inst✝² : TopologicalSpace X✝
space : TCOr (Vec R X✝) (DiscreteTopology X✝)
W : Type u_3
inst✝¹ : Vec R W
X : Type u_2
inst✝ : Vec R X
φ : W → 𝒟 X
x : W → X
hφ : CDifferentiable R φ
hx : CDifferentiable R x
w : W
⊢ CDifferentiableAt R (fun w => (φ w) (x w)) w
no goals