no goals
R : Type u_1
V : Type u_2
W : Type u_3
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : TopologicalSpace V
inst✝² : AddCommGroup W
inst✝¹ : Module R W
inst✝ : TopologicalSpace W
f : V →L[R] W
⊢ ↑(toContinuousAffineMap f) 0 = 0
simp