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

State before:
X : Type u_2
R : Type u_1
inst✝¹ : RealScalar R
inst✝ : TopologicalSpace X
space : TCOr (Vec R X) (DiscreteTopology X)
x : X
⊢ IsSmoothLinearMap R fun φ => φ x
Tactic:
constructor <;> fun_prop
State after:
no goals