Theorem: SciLean.TestFunctionSpace.eval_CDifferentiable_rule' (SciLean/Core/Distribution/TestFunction.lean)

State before:
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
⊢ CDifferentiable R fun w => (φ w) (x w)
Tactic:
intro w
State after:
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

State before:
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
Tactic:
fun_prop
State after:
no goals